cost_ceiling_report
The cost ceiling report definition produces a compliance string for an input source by invoking a certificate that checks whether the net GIVE minus REGIVE balance stays at most 4 in absolute value inside each 8-tick window. LNAL adapter developers and ledger auditors cite it when generating human-readable outputs from Recognition Science cost constraints. The body is a one-line wrapper that builds the certificate and branches on its boolean flag to emit either an OK message or the error list.
claimFor a source string $s$, the cost-ceiling report is the string ``OK: Cost ceiling respected ($|net(GIVE)-REGIVE|≤4)$'' when the derived certificate confirms the bound, and otherwise the semicolon-separated list of error strings carried by the certificate.
background
Recognition Science tracks ledger balance via the net function, defined as total debit minus total credit and required to vanish for any closed ledger. The CostCeilingCert structure packages a boolean flag together with an error list to certify that the absolute net difference between GIVE and REGIVE operations remains at most 4 inside every 8-tick period. The present definition lives in the LNALReports adapter module and simply renders that certificate as a readable string, depending on the Cost quantity type and the two net lemmas imported from the RRF and RSNative layers.
proof idea
The definition calls CostCeilingCert.fromSource on the input string, then applies a direct if-then-else on the resulting ok field: true yields the fixed OK message quoting the bound, false yields the interpolated error list. No lemmas are invoked beyond the certificate constructor itself.
why it matters in Recognition Science
This definition supplies the reporting surface for cost-ceiling checks inside URC adapters, thereby exposing the eight-tick octave bound (T7) to LNAL compilation pipelines. It sits downstream of the net balance lemmas and the CostCeilingCert structure but has no recorded users yet, so its role in closing larger invariant reports remains open.
scope and limits
- Does not prove that any concrete source satisfies the ceiling bound.
- Does not compute net balances itself; delegates entirely to the certificate.
- Does not accept or validate sources outside the LNAL format expected by fromSource.
- Does not return numeric values or quantitative diagnostics, only a pass/fail string.
formal statement (Lean)
34def cost_ceiling_report (src : String) : String :=
proof body
Definition body.
35 let cert := CostCeilingCert.fromSource src
36 if cert.ok then "OK: Cost ceiling respected (|net GIVE−REGIVE| ≤ 4)"
37 else s!"FAIL: {String.intercalate "; " cert.errors}"
38