LocalComposition
LocalComposition encodes the ratio-only composition rule required for a zero-parameter ledger. Researchers bridging T5 J-uniqueness to T6 self-similar fixed points cite this structure when establishing that level composites depend only on adjacent ledger entries. The definition follows immediately from the no-external-scale axiom by setting the compose map to the adjacent ratio and requiring positivity.
claimA local composition on a zero-parameter ledger $L$ is a function $c : ℕ → ℝ$ such that $c(k) = L.levels(k) / L.levels(k+1)$ for every $k$ and $c(k) > 0$.
background
ZeroParameterLedger is the structure whose levels map ℕ to positive reals and whose no-external-scale axiom forces every adjacent ratio to equal the fixed base ratio levels(0)/levels(1). This eliminates all dimensionful parameters and restricts composition rules to pure ratios. The module uses this ledger to derive the locality condition needed for the T5-to-T6 step in the forcing chain, where LocalBinaryRecurrence must hold so that level-(k+2) composites depend only on levels k+1 and k.
proof idea
This is a structure definition. The compose field is set exactly to the adjacent-level ratio supplied by the ledger, the compose_from_levels field records that equality, and compose_positive records the positivity inherited from the ledger's all-positive axiom.
why it matters in Recognition Science
LocalComposition supplies the composition rule consumed by binary_is_minimal, which in turn shows that every ratio equals the base ratio and thereby establishes the binary minimal order required for locality_from_ledger. The structure therefore closes the ledger-to-locality step that justifies the LocalBinaryRecurrence hypothesis in the T5-J-uniqueness to T6-phi-fixed-point bridge.
scope and limits
- Does not admit external scales or dimensionful parameters.
- Does not define compositions that reference levels below k.
- Does not itself prove that the recurrence is binary.
formal statement (Lean)
39structure LocalComposition (L : ZeroParameterLedger) where
40 compose : ℕ → ℝ
41 compose_from_levels : ∀ k, compose k = L.levels k / L.levels (k + 1)
42 compose_positive : ∀ k, 0 < compose k
43