pith. machine review for the scientific record. sign in
structure definition def or abbrev high

of

show as:
view Lean formalization →

The structure bundles the additive J-cost J(x) = (x + x^{-1})/2 - 1 with the three closure axioms on geometric scales and ledger composition. Researchers closing the T5-to-T6 bridge in Recognition Science cite it to force the self-similar ratio r = φ from additivity alone. It is a direct structure definition that imports the cost from the multiplicative recognizer and observer modules with no further reduction steps.

claimThe structure asserts that the cost function $J(x) = (x + x^{-1})/2 - 1$ is additive under ledger composition of independent events at scales $a$ and $b$, so that $J(ab) + J(a/b) = 2J(a)J(b) + 2J(a) + 2J(b)$, and that the resulting scale sequence is closed, forcing the ratio $r$ to satisfy $r^2 = r + 1$.

background

The module derives $r^2 = r + 1$ from three axioms: discrete geometric scales, additive ledger composition (total recognition work adds), and closure under composition. The J-cost is introduced exactly as $J(x) := (x + 1/x)/2 - 1$, which is additive for independent events because the ledger tracks total work rather than multiplicative factors. Upstream results supply the concrete cost: ObserverForcing.cost states that the cost of any recognition event is its J-cost, while MultiplicativeRecognizerL4.cost derives the same function from the comparator on positive ratios.

proof idea

Direct structure definition that composes the J-cost from Cost.Jcost with the ledger factorization from DAlembert.LedgerFactorization.of and the spectral content from SpectralEmergence.of. No tactics appear; the body simply packages the imported cost functions and the three axioms into a single record.

why it matters in Recognition Science

This supplies the J-cost witness that downstream theorems in Action.EulerLagrange and Action.EnergyConservationDomainCert rely on for geodesic and conservation statements, and that Acoustics.SpeechIntelligibilityFromJCost uses for SNR thresholds. It completes the T5 J-uniqueness step that forces φ as the fixed point of the self-similar scale, the same φ that appears in the eight-tick octave and the mass ladder. It leaves open the deeper derivation of closure itself, which is handled in HierarchyDynamics.

scope and limits

formal statement (Lean)

 213structure of J-cost. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.