lambda_rec_is_forced

formal source

 111  · intro h
 112    rw [h]; ring
 113
 114theorem lambda_rec_is_forced :
 115    ∃! lambda : ℝ, lambda > 0 ∧ K lambda = 0 := by
 116  use lambda_rec
 117  constructor
 118  · exact ⟨lambda_rec_pos, lambda_rec_is_root⟩
 119  · intro y ⟨hy_pos, hy_root⟩
 120    exact (lambda_rec_unique_root y hy_pos).mp hy_root
 121
 122/-! ## The Complete G Derivation Chain (Q1 Answer)
 123
 124This section closes the full chain from Q3 cube geometry to κ = 8φ⁵:
 125
 1261. The Q₃ cube has 8 vertices, 12 edges, 6 faces (from DimensionForcing)
 1272. Curvature quanta |κ| = 4 are distributed over 8 faces of S² bounding
 128   each vertex of Q₃, with Gauss-Bonnet normalization χ(S²) = 2
 1293. Balance condition: J_bit = J_curv forces λ_rec = 1/√2 (lambda_0)
 1304. In RS-native units where ℓ₀ = 1, λ_rec = ℓ₀ = 1 (the discrete
 131   lattice sets the scale, absorbing the √2 into the unit convention)
 1325. G = λ_rec² c³ / (π ℏ) with c = 1, ℏ = φ⁻⁵ gives G = φ⁵/π
 1336. κ = 8πG/c⁴ = 8π(φ⁵/π)/1 = 8φ⁵
 134
 135The curvature packet derivation:
 136- Q₃ has 6 faces; each face subtends a dihedral angle of π/2
 137- The total curvature deficit at each vertex: 2π − 3(π/2) = π/2
 138- For 8 vertices: total curvature = 8 × (π/2) = 4π = 2π × χ(S²)
 139- The curvature per unit solid angle normalized by Gauss-Bonnet:
 140  |κ_normalized| = total_curvature / (4π) = 1
 141- Distributing over bounding area 4πλ²: J_curv = 2λ² -/
 142
 143/-- Q₃ cube vertex count. -/
 144def Q3_vertices : ℕ := 8