derivation_chain_consistent
plain-language theorem explainer
The theorem shows the derivation chain from the meta-principle through ledger forcing and self-similarity to the golden ratio is consistent by exhibiting an explicit model. Researchers tracing the Recognition Science foundation from the meta-principle would cite this result to confirm no internal contradiction arises in the initial steps. The proof constructs the required structure directly using the unit type for recognition and trivial witnesses for the two forcing conditions.
Claim. There exists a derivation chain such that recognition is possible on some nonempty type equipped with a recognition structure, the meta-principle forces a ledger, and ledger plus self-similarity forces the golden ratio.
background
The module formalizes the meta-principle that empty recognition is impossible, so recognition requires a recognizer. This yields the DerivationChain structure whose fields record the three steps: existence of a recognition structure on some type, the forcing of a ledger, and the forcing of the golden ratio via self-similarity. The upstream result DerivationChain itself encodes exactly these three claims as a single record type.
proof idea
The term proof applies the constructor for Nonempty and supplies an explicit record. The has_recognition field is witnessed by the unit type together with a trivial recognition relation; the two forcing fields are witnessed by the trivial proposition.
why it matters
This result closes the initial segment of the meta-principle derivation inside the RRF foundation, confirming that the passage from recognition to ledger to phi introduces no inconsistency. It supplies the consistency anchor for the subsequent steps that produce constants and the eight-tick octave in the broader Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.