bsd_implies_phi_irrational
plain-language theorem explainer
The declaration shows that the structural assumption for the Birch-Swinnerton-Dyer conjecture derived from the Recognition Science ledger directly forces the golden ratio to be irrational. Researchers tracing number-theoretic consequences of RS forcing chains would cite this when checking consistency of BSD scaffolds with known irrationality results. The proof is a one-line term application of the defining hypothesis.
Claim. If the structural placeholder for the RS route connecting rank and L-value vanishing order holds, then the golden ratio $phi$ is irrational.
background
The module M-005 supplies a scaffold for components of the Birch-Swinnerton-Dyer conjecture inside Recognition Science. The upstream definition bsd_from_ledger stands for the Prop that encodes the ledger-derived link between elliptic-curve rank and the order of vanishing of the L-function. In the broader framework phi is the self-similar fixed point obtained from the forcing chain after J-uniqueness.
proof idea
The proof is a one-line wrapper that applies the hypothesis directly to obtain the conclusion.
why it matters
The result closes a trivial implication inside the M-005 BSD scaffold. It sits downstream of the ledger placeholder and upstream of any further derivations that would use irrationality of phi to constrain constants or mass ladders. No downstream uses are recorded yet, leaving the scaffold open for additional BSD-to-RS bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.