bornExponentProxy
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the exponent from quantum-mechanical wavefunctions.
- Does not compute lattice energies for named compounds.
- Does not specify exact n for any particular ion pair.
Lean usage
theorem range_check : 10 < bornExponentProxy ∧ bornExponentProxy < 12 := born_exponent_in_rangeformal statement (Lean)
184def bornExponentProxy : ℝ := Constants.phi ^ 5
proof body
Definition body.
185
186/-- The Born exponent proxy is between 10 and 12.
187 φ^5 ≈ 11.09, which matches empirical Born exponents of 9-12. -/