Physics Phi Vs Uniform Pulse Spacing Cert

Pulse spacing and the golden ratio

The golden ratio, often written φ and equal to about 1.618, is a number that appears throughout geometry and art, from the proportions of the Parthenon to the arrangement of leaves on a stem. It is defined as the positive solution to the equation r² = r + 1, which means that multiplying by φ is the same as adding 1. This property makes it a natural choice for a geometric sequence, where each term is a constant multiple of the previous one.

In Recognition Science, the framework models a system as maintaining a ledger, a discrete record of events, and assigns a cost to each step based on the ratio between consecutive intervals. The cost function J(x) = (x + 1/x)/2 - 1 measures how much a ratio deviates from 1, the point of zero cost. A ratio of 1, meaning equal intervals, has zero cost per step, but the framework's boundary conditions force a positive cost at the endpoints of any finite sequence.

The module PhiVsUniformPulseSpacingCert.lean establishes three facts. First, it proves that the ratio of adjacent φ-spaced intervals is exactly φ, by definition. Second, it proves that the cost of a φ-ratio step is positive, and specifically that J(φ) is less than J(2), showing φ is cheaper than a doubling ratio. Third, it defines a prediction, called ExperimentAPrediction, which states that for any positive starting interval and any step index, the cost of the φ-ratio step is positive, and it proves this prediction holds.

The honest claim is more subtle than a simple win for φ. Uniform spacing has zero cost per step, but the boundary conditions mean a finite train of uniform pulses still carries a positive total cost. The φ-ladder reduces this boundary cost because each step is a small, positive deviation from equilibrium, rather than a large jump. The module proves J(φ) < J(2), but the claim that φ is optimal among all ratios r ≠ 1 and r ≠ φ is a MODEL claim, not a theorem.

What this means in plain language: if you must space pulses so that the total cost is minimized, the framework says a geometric sequence with ratio φ beats a uniform sequence, because the uniform sequence pays a large cost at its endpoints. The machine-checked library of formal theorems confirms the arithmetic: the ratio is φ, the cost per step is positive, and φ beats 2. The broader claim that φ is the best of all possible ratios remains a modeling assumption, not a proved result.

/-- Ratio of adjacent φ-spaced intervals = φ. -/
theorem phiSpaced_ratio (τ₀ : ℝ) (hτ₀ : 0 < τ₀) (k : ℕ) :
    phiSpacedInterval τ₀ (k + 1) / phiSpacedInterval τ₀ k = phi := by
  unfold phiSpacedInterval
  have hpos := mul_pos hτ₀ (pow_pos phi_pos k)
  rw [pow_succ, div_eq_iff hpos.ne']
  ring

/-- J-cost of the φ-spacing ratio: J(φ) > 0. -/
theorem phiSpacing_jcost_pos : 0 < Jcost phi :=
  Jcost_pos_of_ne_one phi phi_pos phi_ne_one

/-- φ minimises J among ratios > 1 of "comparable" scale (proved: J(φ) < J(2)). -/
theorem phi_beats_2 : Jcost phi < Jcost 2 := by
  rw [Jcost_eq_sq phi_ne_zero, Jcost_eq_sq (by norm_num : (2 : ℝ) ≠ 0)]
  rw [div_lt_div_iff₀ (by exact mul_pos (by norm_num) phi_pos) (by norm_num)]
  nlinarith [phi_gt_onePointSixOne, phi_lt_onePointSixTwo, phi_sq_eq]

/-- Under RS, the φ-spacing ratio has positive J-cost per step (off-equilibrium drive). -/
theorem experiment_a_prediction_holds :
    ExperimentAPrediction := by
  intro τ₀ hτ₀ k
  rw [phiSpaced_ratio τ₀ hτ₀ k]
  exact phiSpacing_jcost_pos

/-- Uniform spacing has zero step-cost (ratio = 1). -/
theorem uniform_step_cost : Jcost 1 = 0 := Jcost_unit0

What this page does not claim

The claim that φ is optimal among all ratios r ≠ 1 and r ≠ φ is a MODEL claim, not a theorem. The module does not prove that φ-spaced pulses have lower total cost than uniform pulses, only that the per-step cost is positive and less than the cost of a doubling ratio.

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/Physics/PhiVsUniformPulseSpacingCert.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: