NB. =============================================================================
NB. Foundry F1 — AceCertificate math (PURE J)
NB. Copyright (C) 2026 Foundry / Prime Materia Commons
NB.
NB. This program is free software: you can redistribute it and/or modify
NB. it under the terms of the GNU Affero General Public License as published
NB. by the Free Software Foundation, either version 3 of the License, or
NB. (at your option) any later version.
NB.
NB. This program is distributed in the hope that it will be useful,
NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
NB. GNU Affero General Public License for more details.
NB.
NB. You should have received a copy of the GNU Affero General Public License
NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
NB. =============================================================================
NB.
NB. Contract: spec/J_API.md § ace_*; PROPERTIES §H (53–54); j/BOXING.md.
NB. AceCert open fields: lipschitz_upper ; safety_margin ; tail_bound ; certified
NB. ace_certify returns <AceCert>.
NB. Verbs: ace_safety_margin ace_tail_bound ace_certify

cocurrent 'foundry'

NB. max_q ace_safety_margin epsilon → (1-ε) - max_q  (PROPERTIES 53)
ace_safety_margin =: 4 : '(1 - y) - x'

NB. tail_norm ace_tail_bound max_q → tail/(1-max_q) or _ if max_q>=1 (PROPERTIES 54)
ace_tail_bound =: 4 : 0
  if. y >: 1 do. _ else. x % 1 - y end.
)

NB. steps ace_certify delta
NB. steps = list of <StepInfo> (same packing as rec_run history)
NB. Returns <AceCert>
ace_certify =: 4 : 0
  steps =. boxxopen x
  delta =. y
  if. 0 = # steps do. < 0 ; 0 ; 0 ; 0 return. end.
  qs =. 0 $ 0.
  rs =. 0 $ 0.
  for_s. steps do.
    info =. > s
    qs =. qs , 1 {:: info
    rs =. rs , 6 {:: info
  end.
  max_q =. >./ qs
  max_resid =. >./ rs
  eps =. 2 {:: > 0 { steps
  margin =. max_q ace_safety_margin eps
  tail =. max_resid ace_tail_bound max_q
  certified =. margin >: delta
  < max_q ; margin ; tail ; certified
)

cocurrent 'base'