Encyclopedia Foundation Foundation Measure Forcing Cont Weight Eq Phi Rpow Neg
ARTICLE 5 claims 4 theorems 1 hypothesis
Foundation Measure Forcing Cont Weight Eq Phi Rpow Neg
A single rule governs how much weight each recognition state carries, and the framework proves it must be a geometric decay with the golden ratio as its base.
The forced weighting rule
The declaration contWeight_eq_phi_rpow_neg establishes a precise weighting rule for recognition states: the weight assigned to a state with cost t is φ⁻ᵗ, where φ is the golden ratio, approximately 1.618. In plain terms, this means each unit increase in cost reduces the state's weight by a factor of about 0.618, the reciprocal of the golden ratio. This is a geometric decay, not an arbitrary choice; the framework proves it is the only possible weighting that satisfies two plain conditions.
The first condition is factorization: the weight of a composite of independent recognition steps must be the product of the individual weights. This mirrors how probabilities combine for independent events. The second is a self-similar balance condition: the single-step weight ρ must satisfy ρ = 1/(1+ρ), a reciprocal fixed point. Conditional on that equation, the framework proves ρ must equal φ⁻¹. From these two premises, the theorem continuum_weight_forced derives the full function f(t) = φ⁻ᵗ for all t ≥ 0, not just within a restricted class of functions. The proof uses the multiplicative Cauchy equation plus monotonicity to pin the function on the rationals by roots and on the irrationals by an elementary squeeze argument.
This weighting rule is the framework's answer to a missing primitive: given the allowed recognition states, which rule says how much of reality sits in each one? The framework's library of machine-checked theorems shows this geometric measure is the unique stationary weighting. It also yields concrete structure constants: the partition function Z = Σ φ⁻ⁿ = φ², the ground-state share P(0) = φ⁻², and the mean occupied rung ⟨n⟩ = φ exactly. These are proved identities, not fitted parameters.
In Recognition Science, this measure is identified with several previously separate dilution and occupancy laws across the framework: the kernel rung dilution, the dimension dilution, and the constants θ = φ⁻⁴, ℏ = φ⁻⁵, and the rung-44 scale φ⁻⁴⁴. Five separate laws become one object: the forced measure. The framework's library proves these identifications as theorems.
What this declaration does not claim is equally important. It does not claim that any physical recognition weight must satisfy the self-similar balance premise; that remains a hypothesis with a named falsifier. It does not claim to derive the Born rule of quantum mechanics; the full bridge to recognition Hilbert space remains open. And it does not claim that the weighting rule is the only possible one without the two premises; the uniqueness is conditional on them. The framework's honesty about these limits is part of its method: it states plainly what is proved, what is hypothesized, and what remains open.
THEOREM continuum_weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **T9, CONTINUUM LAYER (full uniqueness).** Any factorizing, antitone
weight with the calibrated step `f(1) = φ⁻¹` equals `φ⁻ᵗ` at every
`t ≥ 0`. No power-law-class restriction: this is the multiplicative
Cauchy equation pinned by monotonicity. -/
theorem continuum_weight_forced (hadd : Factorizes f)
(hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho) :
∀ t : ℝ, 0 ≤ t → f t = rho ^ t := by
intro t ht
rcases eq_or_lt_of_le ht with h0 | hpos
· rw [← h0, Real.rpow_zero]
exact f_zero hadd hanti hstep
-- t > 0. Set L := f t and squeeze with rationals.
set L : ℝ := f t with hL
-- upper rationals: t ≤ q ⇒ ρ^q ≤ L
have hub : ∀ q : ℚ, t ≤ (q : ℝ) → rho ^ ((q : ℝ)) ≤ L := by
intro q hq
have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_trans hpos.le hq
have := hanti (Set.mem_Ici.mpr hpos.le) (Set.mem_Ici.mpr hq0) hq
rwa [f_ratCast hadd hanti hstep q hq0] at this
-- lower rationals: 0 ≤ q ≤ t ⇒ L ≤ ρ^q
have hlb : ∀ q : ℚ, 0 ≤ (q : ℝ) → (q : ℝ) ≤ t → L ≤ rho ^ ((q : ℝ)) := by
intro q hq0 hq
have := hanti (Set.mem_Ici.mpr hq0) (Set.mem_Ici.mpr hpos.le) hq
rwa [f_ratCast hadd hanti hstep q hq0] at this
-- L > 0
have hLpos : 0 < L := by
obtain ⟨q, hq⟩ := exists_rat_gt t
exact lt_of_lt_of_le (Real.rpow_pos_of_pos rho_pos _) (hub q hq.le)
have hrt_pos : 0 < rho ^ t := Real.rpow_pos_of_pos rho_pos t
have hlogrho_neg : Real.log rho < 0 := Real.log_neg rho_pos rho_lt_one
-- trichotomy
rcases lt_trichotomy L (rho ^ t) with hlt | heq | hgt
· -- L < ρ^t: find rational q > t with ρ^q > L. Contradiction with hub.
exfalso
have hlog : Real.log L < t * Real.log rho := by
have := Real.log_lt_log hLpos hlt
rwa [Real.log_rpow rho_pos] at this
have hkey : t < Real.log L / Real.log rho := by
rw [lt_div_iff_of_neg hlogrho_neg]
linarith [hlog]
obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hkey
have hcontra : L < rho ^ ((q : ℝ)) := by
have hq2' : Real.log L < (q : ℝ) * Real.log rho := by
have := (lt_div_iff_of_neg hlogrho_neg).mp hq2
linarith
have : Real.exp (Real.log L) < Real.exp (Real.log rho * (q : ℝ)) := by
rw [Real.exp_lt_exp]; linarith
rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this
exact absurd (hub q hq1.le) (not_le.mpr hcontra)
· exact heq
· -- L > ρ^t: find rational 0 ≤ q < t with ρ^q < L. Contradiction with hlb.
exfalso
have hlog : t * Real.log rho < Real.log L := by
have := Real.log_lt_log hrt_pos hgt
rwa [Real.log_rpow rho_pos] at this
have hkey : Real.log L / Real.log rho < t := by
rw [div_lt_iff_of_neg hlogrho_neg]
linarith [hlog]
have hmax : max (Real.log L / Real.log rho) 0 < t := max_lt hkey hpos
obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hmax
have hq0 : (0 : ℝ) ≤ (q : ℝ) :=
le_of_lt (lt_of_le_of_lt (le_max_right _ _) hq1)
have hcontra : rho ^ ((q : ℝ)) < L := by
have hqgt : Real.log L / Real.log rho < (q : ℝ) :=
lt_of_le_of_lt (le_max_left _ _) hq1
have hq2' : (q : ℝ) * Real.log rho < Real.log L := by
have := (div_lt_iff_of_neg hlogrho_neg).mp hqgt
linarith
have : Real.exp (Real.log rho * (q : ℝ)) < Real.exp (Real.log L) := by
rw [Real.exp_lt_exp]; linarith
rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this
exact absurd (hlb q hq0 hq2.le) (not_le.mpr hcontra)
THEOREM partitionZ · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- The partition function `Z = Σ_{n≥0} φ⁻ⁿ`. -/
def partitionZ : ℝ := ∑' n : ℕ, rho ^ n
THEOREM meanRung_eq_phi · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **`⟨n⟩ = φ` exactly.** The mean recognition depth of the forced
measure is the golden ratio itself. -/
theorem meanRung_eq_phi : meanRung = Constants.phi := by
unfold meanRung
have hre : (fun n : ℕ => (n : ℝ) * probMass n)
= fun n : ℕ => (1 - rho) * ((n : ℝ) * rho ^ n) := by
funext n; unfold probMass; ring
rw [hre, tsum_mul_left]
have hnorm : ‖rho‖ < 1 := by
rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one
rw [tsum_coe_mul_geometric_of_norm_lt_one hnorm]
-- (1 − ρ) · ρ/(1−ρ)² = ρ/(1−ρ) = φ⁻¹·φ² = φ
rw [one_sub_rho]
unfold rho
have hphi : Constants.phi ≠ 0 := phi_ne_zero
field_simp
THEOREM latticeWeight · latticeWeight · latticeWeight · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- The lattice weight: `w(n) = φ⁻ⁿ` after `n` recognition steps. -/
def latticeWeight (n : ℕ) : ℝ := (1 / Constants.phi) ^ n
HYPOTHESIS weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **T9, LATTICE LAYER: the weight rule is forced to `φ⁻ⁿ`.** -/
theorem weight_forced (R : RecognitionWeightRule) (n : ℕ) :
R.w n = latticeWeight n :=
(R.toRungDilution).occ_forced n
What this page does not claim
The self-similar balance premise is not proved; it is a hypothesis with a named falsifier. The Born rule of quantum mechanics is not derived from this measure; the bridge to recognition Hilbert space remains open. The identification of the partition function with the Noa voice-density threshold is an observation, not a proved theorem.
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/MeasureForcing.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:
- What is the physical mechanism that would force the self-similar balance premise to hold for actual recognition weights?
- Can the forced measure be extended to a full Born rule on recognition Hilbert space, and what would that require?
- Does the framework's dynamical evolution converge to this stationary weighting, and what would that convergence imply for cosmology?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM continuum_weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **T9, CONTINUUM LAYER (full uniqueness).** Any factorizing, antitone weight with the calibrated step `f(1) = φ⁻¹` equals `φ⁻ᵗ` at every `t ≥ 0`. No power-law-class restriction: this is the multiplicative Cauchy equation pinned by monotonicity. -/ theorem continuum_weight_forced (hadd : Factorizes f) (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho) : ∀ t : ℝ, 0 ≤ t → f t = rho ^ t := by intro t ht rcases eq_or_lt_of_le ht with h0 | hpos · rw [← h0, Real.rpow_zero] exact f_zero hadd hanti hstep -- t > 0. Set L := f t and squeeze with rationals. set L : ℝ := f t with hL -- upper rationals: t ≤ q ⇒ ρ^q ≤ L have hub : ∀ q : ℚ, t ≤ (q : ℝ) → rho ^ ((q : ℝ)) ≤ L := by intro q hq have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_trans hpos.le hq have := hanti (Set.mem_Ici.mpr hpos.le) (Set.mem_Ici.mpr hq0) hq rwa [f_ratCast hadd hanti hstep q hq0] at this -- lower rationals: 0 ≤ q ≤ t ⇒ L ≤ ρ^q have hlb : ∀ q : ℚ, 0 ≤ (q : ℝ) → (q : ℝ) ≤ t → L ≤ rho ^ ((q : ℝ)) := by intro q hq0 hq have := hanti (Set.mem_Ici.mpr hq0) (Set.mem_Ici.mpr hpos.le) hq rwa [f_ratCast hadd hanti hstep q hq0] at this -- L > 0 have hLpos : 0 < L := by obtain ⟨q, hq⟩ := exists_rat_gt t exact lt_of_lt_of_le (Real.rpow_pos_of_pos rho_pos _) (hub q hq.le) have hrt_pos : 0 < rho ^ t := Real.rpow_pos_of_pos rho_pos t have hlogrho_neg : Real.log rho < 0 := Real.log_neg rho_pos rho_lt_one -- trichotomy rcases lt_trichotomy L (rho ^ t) with hlt | heq | hgt · -- L < ρ^t: find rational q > t with ρ^q > L. Contradiction with hub. exfalso have hlog : Real.log L < t * Real.log rho := by have := Real.log_lt_log hLpos hlt rwa [Real.log_rpow rho_pos] at this have hkey : t < Real.log L / Real.log rho := by rw [lt_div_iff_of_neg hlogrho_neg] linarith [hlog] obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hkey have hcontra : L < rho ^ ((q : ℝ)) := by have hq2' : Real.log L < (q : ℝ) * Real.log rho := by have := (lt_div_iff_of_neg hlogrho_neg).mp hq2 linarith have : Real.exp (Real.log L) < Real.exp (Real.log rho * (q : ℝ)) := by rw [Real.exp_lt_exp]; linarith rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this exact absurd (hub q hq1.le) (not_le.mpr hcontra) · exact heq · -- L > ρ^t: find rational 0 ≤ q < t with ρ^q < L. Contradiction with hlb. exfalso have hlog : t * Real.log rho < Real.log L := by have := Real.log_lt_log hrt_pos hgt rwa [Real.log_rpow rho_pos] at this have hkey : Real.log L / Real.log rho < t := by rw [div_lt_iff_of_neg hlogrho_neg] linarith [hlog] have hmax : max (Real.log L / Real.log rho) 0 < t := max_lt hkey hpos obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hmax have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_of_lt (lt_of_le_of_lt (le_max_right _ _) hq1) have hcontra : rho ^ ((q : ℝ)) < L := by have hqgt : Real.log L / Real.log rho < (q : ℝ) := lt_of_le_of_lt (le_max_left _ _) hq1 have hq2' : (q : ℝ) * Real.log rho < Real.log L := by have := (div_lt_iff_of_neg hlogrho_neg).mp hqgt linarith have : Real.exp (Real.log rho * (q : ℝ)) < Real.exp (Real.log L) := by rw [Real.exp_lt_exp]; linarith rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this exact absurd (hlb q hq0 hq2.le) (not_le.mpr hcontra)the theorem continuum_weight_forced derives the full function f(t) = φ⁻ᵗ for all t ≥ 0 continuum_weight_forced · IndisputableMonolith/Foundation/MeasureForcing.leanTHEOREM partitionZ · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- The partition function `Z = Σ_{n≥0} φ⁻ⁿ`. -/ def partitionZ : ℝ := ∑' n : ℕ, rho ^ nthe partition function Z = Σ φ⁻ⁿ = φ² partitionZ · IndisputableMonolith/Foundation/MeasureForcing.leanTHEOREM meanRung_eq_phi · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **`⟨n⟩ = φ` exactly.** The mean recognition depth of the forced measure is the golden ratio itself. -/ theorem meanRung_eq_phi : meanRung = Constants.phi := by unfold meanRung have hre : (fun n : ℕ => (n : ℝ) * probMass n) = fun n : ℕ => (1 - rho) * ((n : ℝ) * rho ^ n) := by funext n; unfold probMass; ring rw [hre, tsum_mul_left] have hnorm : ‖rho‖ < 1 := by rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one rw [tsum_coe_mul_geometric_of_norm_lt_one hnorm] -- (1 − ρ) · ρ/(1−ρ)² = ρ/(1−ρ) = φ⁻¹·φ² = φ rw [one_sub_rho] unfold rho have hphi : Constants.phi ≠ 0 := phi_ne_zero field_simpthe mean occupied rung ⟨n⟩ = φ exactly meanRung_eq_phi · IndisputableMonolith/Foundation/MeasureForcing.leanTHEOREM latticeWeight · latticeWeight · latticeWeight · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- The lattice weight: `w(n) = φ⁻ⁿ` after `n` recognition steps. -/ def latticeWeight (n : ℕ) : ℝ := (1 / Constants.phi) ^ nthe constants θ = φ⁻⁴, ℏ = φ⁻⁵, and the rung-44 scale φ⁻⁴⁴ are identified with the forced measure latticeWeight · latticeWeight · latticeWeight · IndisputableMonolith/Foundation/MeasureForcing.leanHYPOTHESIS weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **T9, LATTICE LAYER: the weight rule is forced to `φ⁻ⁿ`.** -/ theorem weight_forced (R : RecognitionWeightRule) (n : ℕ) : R.w n = latticeWeight n := (R.toRungDilution).occ_forced nit does not claim that any physical recognition weight must satisfy the self-similar balance premise weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean