Astrophysics Cosmic Strings From Phi Ladder

The cosmic string estimate

Cosmic strings are hypothetical one-dimensional defects in the fabric of spacetime, relics of phase transitions in the early universe. If they exist, they would be extraordinarily dense threads, and their gravitational pull is characterized by a quantity called tension, often written Gμ (the Newton constant times the string's mass per unit length). Observations of the cosmic microwave background place an upper bound on this tension: Gμ must be less than about 10⁻⁷.

In Recognition Science, the framework claims a specific formula for this tension: Gμ = J(φ) × (Λ_string/M_Pl)², where Λ_string is the energy scale at which strings formed and M_Pl is the Planck mass. The factor J(φ) comes from the framework's universal cost function J(x) = (x + 1/x)/2 - 1, evaluated at the golden ratio φ ≈ 1.618. If strings formed at the grand unified theory (GUT) scale, this formula yields Gμ between 10⁻⁶ and 10⁻⁷, which is consistent with the observational bound.

What the machine-checked library of formal theorems actually proves is narrower. The library defines a domain cost as J(m/e), a ratio of two masses, and proves three general facts: the cost vanishes when the two masses are equal, it is nonnegative for positive inputs, and the quantity φ - 3/2 is positive. These are properties of the cost function itself, not of cosmic strings.

In plain terms, the library establishes that the framework's cost function has the basic mathematical hygiene one would expect, and that a certain threshold value is positive. What it does not do is connect that cost function to cosmic strings, because the library never defines what m and e mean for a cosmic string. The formula in the research note is an aspiration, not a result.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

What this page does not claim

The library does not prove that cosmic strings exist or that the formula Gμ = J(φ) × (Λ_string/M_Pl)² is correct. The library does not define what m and e mean in the context of cosmic strings.

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/Astrophysics/CosmicStrings_FromPhiLadder.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: