pith. sign in
module module high

IndisputableMonolith.Meta.LedgerUniqueness

show as:
view Lean formalization →

The Meta.LedgerUniqueness module assembles definitions and uniqueness theorems for the RS ledger, centered on the golden ratio as fixed point and Gray-code cycle minimality for the 3-cube. Researchers verifying the forcing chain would cite it to ground T6 and T7. The module combines imported constants and recursive Gray-code constructions with local algebraic checks for fixed-point uniqueness and minimal period.

claim$φ = (1 + √5)/2$ is the unique fixed point of the cost function. The linking dimension of the 3-cube is unique and the binary-reflected Gray code yields a minimal cycle of length 8 on the hypercube.

background

The module sits in the meta layer and imports the RS time quantum τ₀ = 1 tick together with the binary-reflected Gray code whose recursive definition BRGC(0) = [0] produces Hamiltonian cycles on the d-dimensional hypercube. Its own doc-comment states the golden ratio φ = (1 + √5)/2. Local objects include linkingNumber, H_LinkingDimensionUniqueness, Q3_unique_linking_dimension, cube_uniqueness, grayCodeCycleLength, eight_tick_minimal and no_shorter_cycle.

proof idea

The module is a collection of definitions and short algebraic theorems. Fixed-point results are obtained by direct substitution into the cost equation. Cycle-length claims apply the recursive Gray-code construction imported from Patterns.GrayCode to establish that no shorter period exists for the 3-dimensional case.

why it matters in Recognition Science

The results supply the uniqueness statements required by the forcing chain at T6 (phi as self-similar fixed point) and T7 (eight-tick octave). They underwrite the ledger construction by confirming that the linking dimension for Q3 is unique and that the Gray-code cycle is minimal.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (17)