trivialClaim
plain-language theorem explainer
Constantly-true claim on real realizations: the predicate holds everywhere. It is the Forced-branch witness in the maximal-forcing trichotomy demo over the golden-only class. The body is a one-line definition of the always-true predicate, not a derived argument.
Claim. Define a reality claim on $\mathbb{R}$ whose audit label is "True (forced everywhere)" and whose holding predicate is $r \mapsto \top$ for every realization $r$. Equivalently, the claim is true in every real realization.
background
A reality claim is a pair of audit metadata and a predicate on realizations: holds : R → Prop. Forcedness on an admissible class means the predicate is true at every admissible point.
This module sits in Phase 4 of maximal forcing. Earlier layers exercise Forced (cost, phi, dimension, alpha) and Independent (mass yardstick). Here the golden-only class of ratios with $r^2 = r + 1$ is taken without a positivity cut. Over that class, "$r = \varphi$" is not forced because the conjugate root $\psi = (1-\sqrt{5})/2$ also satisfies the constraint; positivity is the named selection principle that drains Selected into Forced.
The constantly-true claim is the trivial Forced pole of that trichotomy, paired later with a Selected claim ("$r = \varphi$") and an Independent claim ("$r > 0$").
proof idea
Definitional, not a proof. The structure fields are filled by a fixed label string and the constant predicate fun _ => True. No lemmas are applied; downstream forcedness is immediate introduction plus trivial.
why it matters
Gives a non-vacuous Forced inhabitant so the classifier is not secretly always-Selected or always-Independent. Downstream, trivialClaim_forced shows it is Forced on the golden-only admissible class; triUniverse packages it with the Selected and Independent claims; all_three_branches_realized cites all three together as the completeness and non-degeneracy certificate for the maximal-forcing machinery.
In framework terms this is scaffolding hygiene for the forcing trichotomy that sits above the T5–T8 chain (J-uniqueness, phi, eight-tick, D = 3): it does not derive those landmarks, but keeps the Forced/Selected/Independent tags honest when selection principles (here positivity) drain interim Selected tags into Forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.