LedgerConfig
plain-language theorem explainer
LedgerConfig packages N positive real ratios into a single data structure for J-cost analysis. Complexity theorists in Recognition Science cite it when bounding verification time for balanced ledgers. The declaration is a direct structure definition that pairs a Fin-indexed function with its positivity predicate.
Claim. For each natural number $N$, a ledger configuration consists of a function $r : [N] → ℝ$ together with the condition that $r(i) > 0$ for every index $i$.
background
The module IC-005 treats physics complexity through J-cost minimization. J(x) = (x + 1/x)/2 − 1 is strictly convex with unique minimum at x = 1. A ledger is a finite collection of recognition states whose total cost is the sum of individual J values. Upstream, LedgerFactorization.of supplies the multiplicative structure on positive reals, MultiplicativeRecognizerL4.cost derives the comparator cost, and ObserverForcing.cost identifies recognition cost with J-cost. SpectralEmergence.of and PhiForcingDerived.of fix the gauge and rung structure that later assign physical meaning to the ratios.
proof idea
Structure definition. The declaration itself introduces the type LedgerConfig N by bundling the ratio map with the positivity axiom; no tactics or lemmas are applied.
why it matters
LedgerConfig supplies the input type for totalJCost, total_jcost_nonneg (IC-005.9), and verification_equivalence (IC-005.11). These results establish that ground-state balance is equivalent to a single sum equaling zero, hence linear-time verifiable. The structure therefore anchors the claim that J-cost minimization is in P while φ-rung computations remain EXPTIME. It directly supports the module’s summary that local 8-tick dynamics are O(1) per step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.