is_self_similar
plain-language theorem explainer
A discrete ledger L is self-similar at ratio r precisely when a SelfSimilar witness exists whose ratio field equals r. Researchers deriving scale invariance from discrete ledger structures cite this definition to introduce the self-similarity hypothesis. It is realized as a direct existential wrapper over the SelfSimilar structure.
Claim. A discrete ledger $L$ is self-similar at scale ratio $r$ if there exists a self-similar structure $S$ such that the ratio of $S$ equals $r$.
background
DiscreteLedger is a structure that pairs a LedgerForcing.Ledger with a DiscretenessForcing.DiscreteConfigSpace, supplying the finite-step configuration space required for the ledger. SelfSimilar is the structure that records a positive ratio not equal to one together with a closed geometric scale sequence witnessing scale invariance. The module PhiForcing shows that self-similarity on a discrete ledger equipped with J-cost forces the scale ratio to obey the equation $x^2 = x + 1$.
proof idea
One-line wrapper that applies the existential quantification over SelfSimilar structures with matching ratio.
why it matters
This definition supplies the hypothesis for the downstream theorem phi_forced, which concludes that any self-similar discrete ledger must have scale ratio exactly φ. It encodes the self-similar fixed-point step (T6) in the forcing chain, where the Recognition Composition Law together with J-cost zero at unity selects the golden ratio as the unique non-trivial solution. The parent theorem phi_forced then invokes golden_constraint_unique to finish the derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.