scaleLedger
plain-language theorem explainer
For any recognition ledger on a finite lattice and any scale λ ≥ 1, every pairwise cost is multiplied by λ and the four ledger axioms still hold. Horizon-preflight arguments cite this family to show boundary cost scales continuously. The nontrivial check is RCL subadditivity, which reduces to λ² ≥ λ together with nonnegativity of costs.
Claim. Let $L$ be a recognition ledger on a finite lattice $\Lambda$ (symmetric nonnegative costs, zero diagonal, RCL-subadditive). For every real $\lambda \ge 1$, the map $(i,j)\mapsto \lambda\, L(i,j)$ is again a recognition ledger on $\Lambda$.
background
A recognition ledger is a real-valued cost on pairs from a finite lattice $\Lambda$: symmetric, zero on the diagonal, nonnegative, and RCL-subadditive. RCL subadditivity is the ledger form of the Recognition Composition Law gate: costs along a two-step path are controlled by the bilinear expression $2uv+2u+2v$ familiar from $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
This module is a falsifier-gated preflight for a model horizon-absorption mechanism (Pillar 3 of Seven Gaps). Existing capital supplies continuous horizon area and a real-valued boundary cost on a substrate bipartition; nothing yet forces area quantization. The scaled ledger is the continuous one-parameter family used to probe whether that boundary cost can carry a uniform spectral gap.
Upstream cost notions (observer J-cost, multiplicative-recognizer cost, rung-coarsen sums) motivate the same nonnegativity and composition structure that the ledger axioms encode; the arithmetic facts used here are ordinary $\mathbb{R}$ inequalities (le_trans, mul_zero).
proof idea
Definitional construction: set cost i j := lam * L.cost i j and discharge the four fields.
- Symmetry: rewrite by the original ledger's symmetry.
- Diagonal zero: original diagonal zero plus
mul_zero. - Nonnegativity: product of
0 ≤ lam(from1 ≤ lam) and the original nonnegativity. - RCL subadditivity: start from the original gate inequality, multiply by
lam ≥ 0, and close withnlinarithusinglam·(2uv+2u+2v) ≤ 2(lam u)(lam v)+2(lam u)+2(lam v), which holds becauselam² ≥ lamforlam ≥ 1and costs are nonnegative.
why it matters
This is the continuous scaling family that drives the P1 ledger falsifier. Downstream, scaleLedger_boundaryCost shows boundary (horizon) cost multiplies exactly by λ, so the family acts continuously on horizon ledger content while preserving every axiom. That identity feeds ledger_boundary_cost_no_uniform_gap: for every claimed gap $g>0$ and every ledger with positive boundary cost, some axiom-preserving scale lands a distinct boundary cost inside $g$.
In the module's capital map this is decisive: discrete-lattice ledger structure does not quantize horizon cost. The candidate absorption comb (area gap $\Delta A = 4\ln\varphi,\ell_P^2$, comb at $GM\omega_*=\ln\varphi/(8\pi)$) therefore remains a model hypothesis, not forced RS capital. Pillar 3 stays open; the dead $0.618$ echo-train route is not revived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.