constantsToJSON
plain-language theorem explainer
constantsToJSON assembles a fixed JSON array of verified constants drawn from Recognition Science, listing values for cone and eight-tick K_net, C_proj, c_min, alpha in ILG, and phi. Report generators in the CPM audit module invoke it to produce exportable verification data. The implementation directly constructs and concatenates a list of JSON object strings without computation.
Claim. The definition yields the string representation of the JSON array containing entries for $K_{net}$ (cone projection) = 1 with source intrinsic cone projection, $K_{net}$ (eight-tick) = $(9/7)^2$ with source covering factor, $C_{proj}$ = 2, $C_{eng}$ = 1, $C_{disp}$ = 1, $c_{min}$ (cone) = 1/2, $c_{min}$ (eight-tick) = 49/162, $alpha$ (ILG) = $(1-1/phi)/2$, and $phi$ = $(1+sqrt{5})/2$.
background
The CPM Constants Audit module supplies machine-checkable verification of constants derived from Recognition Science invariants, including the fundamental tick tau_0 = 1 and structures for J-cost and nuclear densities in phi-tiers. Upstream results include the definition of tick as the RS time quantum from Constants and the structure of J-cost from PhiForcingDerived. This definition supports the export of constant lists for audit reports as described in the module documentation.
proof idea
The definition constructs a list of nine JSON string items, each encoding a constant name, value, source, and exactness flag, then wraps them in an array using String.intercalate. It relies on no external lemmas beyond basic string operations and the imported constants such as tick and phi.
why it matters
This definition supplies the constant data consumed by generateJSONReport to produce the full audit output. It encodes the verified values tied to the eight-tick octave (T7) and phi fixed point (T6) from the forcing chain, enabling checks against the alpha band and mass formula. It closes part of the export infrastructure for the CPM module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.