DerivationChain
plain-language theorem explainer
DerivationChain packages the steps from the meta-principle through ledger forcing to the golden ratio φ. A researcher tracing how recognition axioms yield physical constants would cite this structure to organize the chain. The definition assembles an existential witness for a recognition structure with two placeholder assertions for the subsequent forcing steps.
Claim. A structure consisting of three fields: an existence claim that there is a type $X$ carrying a nonempty RecognitionStructure (a binary relation with a self-recognition witness); the assertion that recognition forces a ledger; and the assertion that ledger structure plus self-similarity forces the golden ratio φ.
background
The module states the Meta-Principle that nothing cannot recognize itself, so recognition requires a recognizer. RecognitionStructure is the minimal carrier with a binary recognizes relation and an existential self-recognition witness. MPForcesLedger is the hypothesis class that adds integer charge assignments and the requirement that nontrivial transactions balance to zero sum.
proof idea
This is a structure definition with no proof body. It simply records the three fields of the derivation claim as a single record type.
why it matters
It supplies the container for the full derivation claim from the meta-principle through ledger and self-similarity to φ, directly feeding the consistency theorem derivation_chain_consistent. The structure aligns with the Recognition Science forcing chain from the meta-principle to the φ fixed point and the eight-tick octave. It leaves open the discharge of the two True placeholders into explicit proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.