SelfSimilar
plain-language theorem explainer
SelfSimilar packages a positive scale ratio different from one that is witnessed by a closed geometric scale sequence. Researchers deriving the golden ratio from self-similarity in discrete ledgers cite this structure. It is introduced as a bare structure definition with no computational content or proof obligations.
Claim. A self-similar structure consists of a real number $r$ satisfying $0 < r$ and $r ≠ 1$, together with the existence of a geometric scale sequence $S$ such that the ratio of $S$ equals $r$ and $S$ is closed.
background
The Phi Forcing module establishes that self-similarity in a discrete ledger equipped with J-cost forces the golden ratio. A geometric scale sequence is a structure carrying a ratio $r > 0$, $r ≠ 1$ together with a sequence of successive scalings. The module argument proceeds by requiring that scaling by $r$ be cost-equivalent to the identity at every level, which is possible only when $r$ satisfies the fixed-point equation of the J-function. Upstream results supply the GeometricScaleSequence definition and the closure property used in the existential witness.
proof idea
This declaration is a structure definition that directly encodes the ratio together with the scale-invariance witness as an existential quantifier over closed geometric sequences from the derived module.
why it matters
The structure is referenced by the self-similarity predicate for discrete ledgers and by the theorem that closed geometric self-similarity forces the golden constraint. It supplies the key object for the main result that any self-similar discrete ledger must have scale ratio equal to φ. This realizes the T6 step of the forcing chain in which phi appears as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.