gap_balance
The phi-power balance identity at D=3 shows that phi raised to (active-edge count minus integration gap) times phi to the gap power equals phi. Recognition Science researchers cite it when verifying exponent closure on the phi-ladder inside mass formulas. The proof is a short tactic sequence that substitutes the precomputed gap value 45, rewrites the active-edge count as 1, and reduces the combined exponent via zpow_add and norm_num.
claim$phi^{1-g}cdot phi^g=phi$ where the active edge count per tick equals 1 and the integration gap $g$ equals 45 at the forced spatial dimension 3.
background
The integration gap is defined as the product of parity count and configuration dimension for a given spatial dimension D. At D=3 this product equals 45. The active edge count per fundamental tick is fixed at 1. The module also establishes that gcd of 2^D with the gap equals 1 precisely when D is odd, which combines with the dimension-forcing argument to select D=3 among odd candidates.
proof idea
The tactic proof first obtains the integer value 45 for the gap at D=3 from the upstream result integrationGap_at_D3. It rewrites the active edge count as 1 and applies zpow_add₀ to combine the exponents. A norm_num step confirms that 1 minus 45 plus 45 equals 1, after which zpow_one produces the right-hand side phi.
why it matters in Recognition Science
This identity supplies the required exponent cancellation for the phi-ladder when the integration gap appears in mass formulas. It sits inside the foundation layer that precedes the mass and actualization modules and is consistent with the eight-tick octave and D=3 selection from the forcing chain. No downstream theorems are listed, so the result functions as a local arithmetic closure check.
scope and limits
- Does not derive the numerical value of the integration gap from axioms.
- Does not extend the identity to any dimension other than D=3.
- Does not connect the balance to the J-cost functional or Recognition Composition Law.
- Does not address physical units or Berry creation threshold.
formal statement (Lean)
109theorem gap_balance :
110 phi ^ (A - ↑(integrationGap D)) * phi ^ (↑(integrationGap D) : ℤ) = phi := by
proof body
Tactic-mode proof.
111 have hg : (↑(integrationGap D) : ℤ) = 45 := by exact_mod_cast integrationGap_at_D3
112 rw [hg, show A = (1 : ℤ) from rfl, ← zpow_add₀ (ne_of_gt phi_pos)]
113 have : (1 : ℤ) - 45 + 45 = 1 := by norm_num
114 rw [this, zpow_one]
115
116end
117
118/-! ## Master certificate -/
119