constantsToJSON
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive constants from the functional equation or RCL.
- Does not perform numerical verification or coincidence bounds.
- Does not include dynamic computation of values from axioms.
- Limited to the listed constants; omits others like G or hbar.
Lean usage
def generateJSONReport : String := ... ++ constantsToJSON ++ ...formal statement (Lean)
213def constantsToJSON : String :=
proof body
Definition body.
214 let items := [" { \"name\": \"K_net (cone)\", \"value\": \"1\", \"source\": \"Intrinsic cone projection\", \"exact\": true }",
215 " { \"name\": \"K_net (eight-tick)\", \"value\": \"(9/7)^2 = 81/49\", \"source\": \"ε=1/8 covering\", \"exact\": true }",
216 " { \"name\": \"C_proj\", \"value\": \"2\", \"source\": \"Hermitian rank-one bound, J''(1)=1\", \"exact\": true }",
217 " { \"name\": \"C_eng\", \"value\": \"1\", \"source\": \"Standard normalization\", \"exact\": true }",
218 " { \"name\": \"C_disp\", \"value\": \"1\", \"source\": \"Dispersion bound\", \"exact\": true }",
219 " { \"name\": \"c_min (cone)\", \"value\": \"1/2\", \"source\": \"1/(1·2·1)\", \"exact\": true }",
220 " { \"name\": \"c_min (eight-tick)\", \"value\": \"49/162\", \"source\": \"1/((81/49)·2·1)\", \"exact\": true }",
221 " { \"name\": \"α (ILG)\", \"value\": \"(1-1/φ)/2\", \"source\": \"Self-similarity\", \"exact\": true }",
222 " { \"name\": \"φ\", \"value\": \"(1+√5)/2\", \"source\": \"x²=x+1 fixed point\", \"exact\": true }"]
223 "[\n" ++ String.intercalate ",\n" items ++ "\n]"
224
225/-- Generate a JSON array of example certificates. -/