lnal_manifest_json
plain-language theorem explainer
The manifest JSON aggregator for LNAL reports produces a structured JSON output from source code that collects certificate results for invariants, compiler checks, schedule neutrality, cost ceiling, J-monotonicity and units gate, together with delta-J sequences and falsifier flags. Auditors of LNAL implementations cite this aggregator to obtain a single structured report. The definition parses the input, invokes the relevant certificate constructors and static checkers, then serializes the collected data into a nested JSON object.
Claim. The function that maps a source string $s$ to a pretty-printed JSON string containing the conjunction of ok flags from the LNAL invariants certificate, compiler checks certificate, schedule neutrality certificate, cost ceiling certificate, J-monotone report and units gate certificate, together with arrays of delta-J values, phi literal entries, packet data, commit windows, greedy predictions and progress witnesses.
background
The LNALReports module in the URCAdapters layer generates machine-readable manifests for the Certificate Engine v2. Upstream, CostAlgebra.comp composes J-automorphisms that preserve the multiplicative structure of the J-cost function. ConsentCert is the structure that records enabled status, overall ok flag, violation list and message list for gate audits. RSNativeUnits.status documents the native units with tick and voxel as base, speed of light equal to one, coherence quantum equal to phi to the minus five, and the phi-ladder. The local setting is static analysis and reporting for LNAL programs that encode recognition operations.
proof idea
The definition first builds the invariants certificate from the source string. It attempts a full parse of the program and falls back to empty phi analysis and empty packets on error. Static checks are invoked to obtain the compiler checks certificate and J-monotone data. Schedule neutrality, cost ceiling and units gate certificates are constructed directly from the source. The overall ok flag is formed by conjunction of the six certificate ok fields. Lists of phi literals, errors, packets, commit windows, j-greedy entries and progress witnesses are mapped to JSON objects. The top-level object is assembled and passed to pretty-print.
why it matters
This definition realises the manifest output for Certificate Engine v2 and directly feeds ConsentCert construction for derivative audits. In the Recognition framework it operationalises static checks on J-monotonicity and cost ceilings that follow from the forcing chain and the recognition composition law. No parent theorems appear in the used-by graph, leaving open the question of integration into automated verification pipelines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.