bornExponentProxy
plain-language theorem explainer
The Born exponent proxy equals the fifth power of the golden ratio constant. Ionic lattice modelers cite this to connect the empirical Born-Mayer repulsion term (n near 11) to Recognition Science phi values. The definition is a direct assignment from the phi constant in the Constants bundle with no further reduction.
Claim. The proxy for the Born-Mayer repulsion exponent is defined as $n = phi^5$, where $phi$ is the self-similar fixed point of the Recognition Science forcing chain.
background
The IonicBond module derives ionic bonding from 8-tick shell closure: alkali metals donate electrons to halogens to reach noble-gas configurations, with net energy set by ionization cost minus affinity plus Madelung lattice attraction. The Born exponent appears in the short-range repulsion of the lattice potential. Upstream, the phi constant is supplied by the PhiForcingDerived structure that encodes J-cost minimization and by the Constants bundle from LawOfExistence.
proof idea
This is a direct definition bornExponentProxy := Constants.phi ^ 5. It functions as a one-line proxy; downstream range checks apply dsimp followed by linarith on the phi_fifth_bounds lemma.
why it matters
The definition supplies the numerical value used by the downstream born_exponent_in_range theorem to verify 10 < phi^5 < 12, matching the empirical 9-12 range stated in the module doc-comment. It links the chemistry derivations to the core T6 phi fixed point and T7 eight-tick octave of the foundation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.