trivialClaim_forced
plain-language theorem explainer
The always-true reality claim is forced on the golden-constraint class of real ratios (no positivity). Anyone assembling the trichotomy completeness certificate cites this as the Forced witness. The proof is a one-line wrapper: introduce any admissible realization and discharge True.
Claim. Let $\mathcal{L}$ be the class of real ratios $r$ satisfying the golden constraint $r^2=r+1$, with no positivity requirement. The trivial claim $C_\top$ (which holds at every realization) is forced on $\mathcal{L}$: for every $r\in\mathcal{L}$, $C_\top$ holds at $r$.
background
This module sits in Maximal Forcing Phase 4. It exercises the third trichotomy branch, Selected, over the golden-constraint class, and also supplies clean Forced and Independent witnesses so the classifier is non-degenerate.
An admissibility class packages a set of allowed realizations. Here Lgolden is the set of reals $r$ with $r^2=r+1$, strictly looser than the positive golden class (which also demands $0<r$). A reality claim is Forced on an admissible set when it holds at every member: $\forall R_0\in\mathrm{Admissible},, C(R_0)$.
The trivial claim is the constant-true claim: its holding predicate is $\lambda_.,\mathrm{True}$, labeled as forced everywhere. It is the canonical Forced example over any nonempty class.
proof idea
One-line wrapper on the definition of Forced. Unfold Forced to $\forall R_0\in\mathrm{Lgolden.admissible},,\mathrm{trivialClaim.holds},R_0$; introduce the realization and membership hypotheses; the goal is True, discharged by trivial.
why it matters
Supplies the Forced conjunct in all_three_branches_realized, which states that a single closure realizes all three trichotomy branches with proofs (Forced, Selected, Independent) and rules out a secretly always-forced or always-independent classifier. Also feeds triUniverse_classifier, the certificate that over the golden-only class the trivial claim is forced, the phi claim is selected by positivity, and positivity is independent (phi vs psi).
In the module narrative, Forced is already exercised elsewhere by cost, phi, dimension, and alpha; this lemma is the minimal, content-free Forced anchor so the third-branch Selected story (isPhi over Lgolden, drained by positivity to LphiGold) can sit beside genuine Forced and Independent examples without the machinery collapsing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.