inevitability
plain-language theorem explainer
Any zero-parameter alternative framework deriving observables must either match the RS cost and selection or violate at least one necessity gate. Researchers formalizing uniqueness claims in Recognition Science cite this as the precise no-alternatives result. The proof applies excluded middle on cost and selection equality then routes mismatches to the corresponding gate via further case splits and gate membership.
Claim. Let $F$ be an alternative framework with zero parameters that derives observables. Then either the cost functional of $F$ equals the RS cost functional and the selection rule of $F$ equals the RS selection rule, or there exists a necessity gate $g$ in the list of all necessity gates such that $F$ violates $g$.
background
The module formalizes the inevitability structure by relocating degrees of freedom into the cost foundation. An AlternativeFramework is a structure carrying a cost functional from reals to reals, a selection rule from reals to propositions, a natural number of parameters, and a boolean flag for deriving observables. RS_framework is the concrete instance whose cost is the J functional from the law of existence and whose selection is the predicate that defect equals zero.
proof idea
The proof performs case analysis on whether cost and selection of F match those of RS_framework. If they match, the left disjunct is immediate. Otherwise a second case split on cost equality is used: when costs agree but selection differs, gate_selection_rule is exhibited as the violated member of all_gates; when costs differ, gate_cost_uniqueness is exhibited. Each branch closes with simp on the gate list and unfold on violates_gate.
why it matters
This is the central uniqueness theorem of the inevitability structure, feeding directly into full_unconditional_inevitability and the concrete_inevitability record in the equivalence module. It realizes the no-alternatives claim by reducing any deviation to a gate violation. In the broader framework it closes the choke point after T5 J-uniqueness, the eight-tick octave, and the forcing of D=3, ensuring the alpha band and mass ladder emerge without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 4 of 4)
-
Surprise predictor outperforms baselines on spatial video tasks
"Yet performance on VSI-SUPER remains limited, indicating that scale alone is insufficient for spatial supersensing."
-
Hybrid CNN-state space model tops CNNs and Transformers on medical segmentation
"The results reveal that U-Mamba outperforms state-of-the-art CNN-based and Transformer-based segmentation networks across all tasks."
-
Mixup on example pairs improves neural network generalization
"Our experiments on the ImageNet-2012, CIFAR-10, CIFAR-100, Google commands and UCI datasets show that mixup improves the generalization of state-of-the-art neural network architectures."
-
Self-distillation turns feedback into denser RL signals
"The SDPO gradient is a (negated) logit-level policy gradient where the advantages are estimated using the self-teacher."