Foundation Maximal Forcing Rsselection Example

The three-way classification

Consider the equation r² = r + 1. It has two real solutions: the golden ratio φ, which is positive and about 1.618, and ψ, which is negative and about −0.618. Both satisfy the constraint, but only one is positive. This is a classical starting point for asking how much a constraint can determine an answer.

Recognition Science sorts claims about reality into three buckets: forced, independent, or selected. A forced claim holds in every admissible case; an independent claim holds in some and fails in others. A selected claim is neither: it is not forced, but a named principle resolves it. The machine-checked library of formal theorems exercises this third branch with the golden ratio as its example.

The module defines the class Lgolden of ratios satisfying r² = r + 1 with no positivity requirement. Over this class, the claim "r = φ" is not forced: ψ satisfies the constraint and differs from φ. The framework proves this directly. But the claim is not left dangling. A named selection principle, positivity, picks the expanding root greater than 1. The framework proves that "r = φ" is selected over Lgolden, and that adding positivity as a tightening promotes it to forced, which is the theorem forced_isPhi.

The same module builds a universe with three claims at once: a trivial claim that is forced everywhere, the phi claim that is selected, and a positivity claim that is independent. A single certificate classifies all three. This demonstrates that the classification machinery is complete and non-degenerate: it can land a claim in any of the three buckets, not just one.

What this establishes in plain language is that the framework's classification system has real teeth. A claim can be genuinely unresolved by constraints alone, yet still governed by an explicit principle. The selected tag is not an endpoint; it comes with a proved path to forced status. The example shows the system can handle all three outcomes honestly, without collapsing into always-forced or always-independent.

/-- "r = phi" is **not forced** over the golden-only class: the conjugate root is
an admissible counterexample. -/
theorem isPhi_not_forced_over_Lgolden : ¬ Forced Lgolden.admissible isPhiClaim := by
  intro hF
  have hpsi : psi = φ := hF psi psi_golden
  exact psi_ne_phi hpsi

/-- **"r = phi" is Selected over the golden-only class.** Not forced, but governed
by the positivity selection principle. This is the third branch of the trichotomy,
reached honestly. -/
theorem isPhi_selected_over_Lgolden : Selected Lgolden.admissible isPhiClaim :=
  ⟨isPhi_not_forced_over_Lgolden, ⟨positivitySelection⟩⟩

/-- **Drainage of the Selected tag.** Selected is not an endpoint: adopting the
positivity principle as a tightening (`Lgolden → LphiGold`) promotes the claim to
`Forced`. The promotion is exactly `forced_isPhi`. So this Selected entry has a
proved resolution, not a perpetual hold. -/
theorem positivity_promotes_selected_to_forced :
    Selected Lgolden.admissible isPhiClaim ∧
    Nonempty (Tightening Lgolden LphiGold) ∧
    Forced LphiGold.admissible isPhiClaim :=
  ⟨isPhi_selected_over_Lgolden, ⟨tighten_Lgolden_LphiGold⟩, forced_isPhi⟩

/-- **The maximal-forcing machinery is complete and non-degenerate.** A single
closure realizes all three branches of the trichotomy with proofs: one forced, one
selected, one independent. This rules out the failure mode where the classifier is
secretly always-forced or always-independent. -/
theorem all_three_branches_realized :
    Forced Lgolden.admissible trivialClaim ∧
    Selected Lgolden.admissible isPhiClaim ∧
    Independent Lgolden.admissible positiveClaim :=
  ⟨trivialClaim_forced, isPhi_selected_over_Lgolden, positiveClaim_independent⟩

What this page does not claim

The module does not prove that the golden ratio is forced by the constraint alone. The module does not claim that selection principles are derived rather than named. The module does not establish that all claims can be classified into one of the three buckets.

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/MaximalForcing/RSSelectionExample.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: