ZeroParameterLedger
ZeroParameterLedger defines a sequence of positive real levels whose consecutive ratios stay fixed under any positive rescaling. Researchers closing the T5 to T6 bridge in Recognition Science cite this structure to enforce scale-free ledger properties before deriving binary recurrence. The declaration is a direct structure definition with no proof obligations.
claimA zero-parameter ledger consists of a function $l : ℕ → ℝ$ such that $l(n) > 0$ for all $n ∈ ℕ$, and for every $λ > 0$ the ratio $l(n)/l(n+1)$ equals $l(0)/l(1)$ independently of $λ$ and for every $n$.
background
The module LocalityFromLedger derives the local binary recurrence needed for the T5→T6 bridge by starting from ledger properties that admit only dimensionless ratios. ZeroParameterLedger encodes the zero-parameter condition: levels are positive reals and all adjacent ratios are invariant under external positive scaling. This forces any composition rule to be expressible solely in terms of those ratios, as stated in the module's argument that zero parameters imply ratio-only composition.
proof idea
This is a structure definition. It directly encodes the zero-parameter condition via the three fields: the level map, the positivity axiom, and the scale-invariance axiom on ratios.
why it matters in Recognition Science
ZeroParameterLedger is the root assumption for the module's main results. It is used by binary_is_minimal to prove that composition order must be two, by locality_from_ledger to obtain the geometric progression, and by LocalityCert to certify uniformity. In the Recognition framework it supplies the scale-free starting point that lets the forcing chain reach the self-similar fixed point at T6 without introducing external parameters.
scope and limits
- Does not fix the numerical value of the common ratio.
- Does not encode composition rules that reference levels more than one step apart.
- Does not guarantee positivity or boundedness for quantities derived from the levels beyond the stated axioms.
formal statement (Lean)
33structure ZeroParameterLedger where
34 levels : ℕ → ℝ
35 all_positive : ∀ n, 0 < levels n
36 no_external_scale : ∀ (λ : ℝ), λ > 0 →
37 ∀ n, levels n / levels (n + 1) = levels 0 / levels 1
38