Foundation Dimensional Bridge Structural Dimensional Bridge Residual

The dimensional bridge residual

The dimensional bridge is the conversion map that translates Recognition Science's native units into SI units. The declaration DimensionalBridgeResidual packages the current state of that bridge as a formal structure: it states that there exists a positive conversion factor E_coh such that the electron mass in SI units equals E_coh times φ³, where φ is the golden ratio. This is a definitional scaffold, not a derivation. The structure records the relationship that must hold if the bridge is to close, and it does so without claiming that the factor has been computed from first principles.

What the framework's machine-checked library does prove sits around this scaffold. The native electron mass m_e_RS is defined as φ³, and a theorem establishes it lies between 4.22 and 4.24 in coherence-energy units. The SI electron mass is taken from CODATA 2022 as 0.5109989461 MeV, with a proof that this value is positive. From these two, the coherence energy E_coh is defined as the ratio m_e_SI / φ³, and a theorem proves it falls in the band (0.120, 0.122) MeV. A further theorem shows this band sits within 0.013 MeV of J(φ), the framework's cost function evaluated at the golden ratio, which equals φ − 3/2 ≈ 0.118. The bound is loose; the actual proximity is closer to 0.0026 MeV, but the formal proof only guarantees the wider window given the current bounds on φ.

The declaration's own docstring names the honest status: the dimensional bridge residual is a single ratio E_coh = m_e_SI / φ³ whose derivation from RS primitives is the principal open frontier. Two candidate routes are sketched but not proved: deriving a fundamental time unit from a known quantum system, or deriving G = φ⁵/π in SI units and using the Planck mass to set the scale. Neither route is closed. The structure DimensionalBridgeResidual therefore does not assert that the electron mass has been explained; it asserts the shape such an explanation must take.

In plain terms, the declaration is a formal placeholder with proven bounds around it. It establishes that the electron's measured mass, divided by the golden ratio cubed, lands near the framework's characteristic cost value at the MeV scale. It does not establish why that ratio takes the value it does. The gap between the structural form and a full derivation is the residual that gives the declaration its name, and closing it remains the target.

/-- The dimensional bridge residual: a single ratio `E_coh = m_e_SI / φ³`
    whose derivation from RS primitives is the principal open frontier.

    The two candidate routes:
    (a) Derive `τ₀^SI` from a known quantum system, then `E_coh = ℏ / τ₀`.
    (b) Derive `G = φ⁵/π` in SI units, then the Planck mass gives the scale.
-/
structure DimensionalBridgeResidual where
  /-- The conversion factor E_coh in SI units. -/
  E_coh_SI : ℝ
  /-- The conversion factor is positive. -/
  E_coh_pos : 0 < E_coh_SI
  /-- The electron mass formula: m_e_SI = E_coh * φ^3. -/
  electron_mass_formula : m_e_SI_MeV = E_coh_SI * phi ^ 3

/-- Restatement of the electron rung result. -/
theorem m_e_RS_band : 4.22 < m_e_RS ∧ m_e_RS < 4.24 := by
  unfold m_e_RS
  constructor
  · nlinarith [phi_gt_onePointSixOne, phi_sq_eq, sq phi]
  · nlinarith [phi_lt_onePointSixTwo, phi_sq_eq, sq phi]

/-- `E_coh_MeV ∈ (0.120, 0.122)` MeV. -/
theorem E_coh_band : 0.120 < E_coh_MeV ∧ E_coh_MeV < 0.122 := by
  unfold E_coh_MeV m_e_SI_MeV m_e_RS
  constructor
  · rw [lt_div_iff₀ (by nlinarith [phi_gt_onePointSixOne, phi_sq_eq, sq phi] : 0 < phi ^ 3)]
    nlinarith [phi_lt_onePointSixTwo, phi_sq_eq, sq phi]
  · rw [div_lt_iff₀ (by nlinarith [phi_gt_onePointSixOne, phi_sq_eq, sq phi] : 0 < phi ^ 3)]
    nlinarith [phi_gt_onePointSixOne, phi_sq_eq, sq phi]

/-- Proximity to J(φ): |E_coh_MeV - J(φ) · 1 MeV| < 0.013 MeV.

The bound `0.013` is the loose value provable from the `phi ∈ (1.61, 1.62)`
band currently available in `Constants.lean`; the actual numerical proximity
is roughly `0.0026` (computed from `phi ≈ 1.61803`, `m_e_SI/phi^3 ≈ 0.12063`,
`phi - 3/2 ≈ 0.11803`). Tightening this bound requires sharper `phi` bounds. -/
theorem E_coh_near_JPhi :
    |E_coh_MeV - (phi - 3/2)| < 0.013 := by
  unfold E_coh_MeV m_e_SI_MeV m_e_RS
  have ⟨h_lo, h_hi⟩ := E_coh_band
  unfold E_coh_MeV m_e_SI_MeV m_e_RS at h_lo h_hi
  have h_jphi_lo : 0.110 < phi - 3/2 := by linarith [phi_gt_onePointSixOne]
  have h_jphi_hi : phi - 3/2 < 0.120 := by linarith [phi_lt_onePointSixTwo]
  rw [abs_lt]
  constructor <;> linarith

What this page does not claim

The declaration does not derive the electron mass from RS primitives; it only packages the structural form of that derivation as a target. The proximity to J(φ) is a numerical coincidence with a loose formal bound, not a proof that the electron mass is forced by the framework. The structure does not assert that E_coh has a unique value; it only asserts existence of a positive factor satisfying the mass formula.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DimensionalBridgeStructural.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: