Foundation Coherence Exponent Integration Dimension Eq

The integration dimension

In the Recognition Science framework, the integration dimension is a number that counts how many independent variables a physical integration must sum over. The framework's library, a machine-checked collection of formal theorems, defines this count as the number of spatial dimensions plus two. Since the framework forces three spatial dimensions, the count becomes three plus two, which is five. A proved theorem, integrationDimension_eq, states exactly this: the integration dimension equals five.

The number five is not arbitrary. The framework reaches it by two separate routes that agree. One route starts with the three spatial dimensions and the eight-tick period, both forced by earlier theorems. The difference between eight and three is five, and five is a Fibonacci number. The other route counts the integration variables directly: three spatial dimensions, one temporal dimension, and one conservation constraint. Both routes land on five, and the library proves they agree.

This five then appears in the framework's coherence energy exponent. The library defines the coherence energy as the golden ratio raised to the negative fifth power, and it proves this equals the integration dimension. So the integration dimension is not merely a count; it is the same five that appears in the energy exponent, tying the counting of variables to a physical quantity.

What the theorem does not do is prove that the integration dimension must be five from first principles. The theorem proves that the definition, which already sets the dimension to three plus two, evaluates to five. The forcing of the three spatial dimensions comes from other theorems in the framework, and the temporal and conservation additions are part of the definition. The theorem itself is a computation, not a derivation of the dimension count from nothing.

theorem integrationDimension_eq : integrationDimension = 5 := by
  unfold integrationDimension D; norm_num

/-- The number of independent integration variables:
    D spatial + 1 temporal + 1 conservation = D + 2 -/
def integrationDimension : ℕ := D + 2

/-- E_coh = φ^{-5} in rpow form matches the Fibonacci-forced exponent.
    Bridge: cLagLock uses rpow with -(5:ℝ); we show coherenceExp = 5 produces
    the same value via zpow → rpow conversion. -/
theorem E_coh_eq_phi_neg5 : E_coh = phi ^ (-(5 : ℝ)) := by
  unfold E_coh cLagLock; rfl

What this page does not claim

The theorem does not prove that the integration dimension must be five from first principles. It does not claim that the integration dimension is a physically measurable quantity in the conventional sense. It does not derive the value of the golden ratio or the three-dimensionality of space; those are separate results.

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/CoherenceExponent.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: