HasLocalComposition
plain-language theorem explainer
Zero-parameter comparison ledgers admit local binary composition when their level sizes obey a linear recurrence with positive integer coefficients for adjacent levels. Researchers deriving the golden ratio from self-similar dynamics in Recognition Science reference this interface to enforce locality. The declaration is introduced as a class extending HasMultilevelComposition by adding the recurrence levels(2) = a levels(1) + b levels(0) for integers a, b at least 1.
Claim. Let $L$ be a zero-parameter comparison ledger. Then $L$ has local composition if it extends multilevel composition with positive integers $a,b$ satisfying $1$ at least $a$ and $1$ at least $b$, such that the level sizes obey the recurrence $l(2) = a l(1) + b l(0)$, where $l$ is the positive real-valued level function with at least three levels.
background
The ZeroParameterComparisonLedger packages a countable nonempty carrier, an admissible cost satisfying the Recognition Composition Law, a conserved charge, and the absence of free parameters. HasMultilevelComposition supplies the level function $l : ℕ → ℝ$ that is positive and defined for at least three indices. The local variant adds the physical constraint that composition acts only between adjacent levels via integer coefficients. Upstream, CostAxioms.Composition states the d'Alembert equation $F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$ for positive reals. HierarchyRealization.RealizedHierarchy iterates a dynamics operator to produce self-similar level sizes, and HierarchyDynamics.bridge_T5_T6_internal shows that any such realization forces the scale ratio to equal phi.
proof idea
This is a class definition extending HasMultilevelComposition. It adds fields coeff_a and coeff_b together with the positivity axioms and the local recurrence equation on the levels function.
why it matters
This class supplies the local composition interface required for the unconditional inevitability theorem built on the zero-parameter ledger. It feeds the HierarchyDynamics module, where zero-parameter minimality is shown to force coefficients (1,1) and hence phi via bridge_T5_T6_internal. In the Recognition Science framework it supports the step from T5 J-uniqueness to T6 phi fixed point by enforcing locality inside the realized hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Chunk and align method scales 3D model to kilometer videos
"To correct the accumulated drift inherent in sequential estimation, we perform loop closure detection across the entire sequence."