FinalReggeComponentTarget
plain-language theorem explainer
Packages the final target for the arbitrary-triangulation Regge component theorem: every incidence-consistent 3D triangulation admits a concrete component comparison. Gravity workers closing the discrete-to-continuum Regge path cite this Prop. It is a pure definitional wrapper of a universal quantification, not a proof.
Claim. The final Regge component target is the proposition that for every three-dimensional triangulation $K$ satisfying the incidence-consistency condition, the type of concrete component comparisons for $K$ is nonempty.
background
This module sits in the gravity/Regge track. It separates the independent dual-weight construction (edge-pair incidence weights and vertex-pair hinge weights on a 3D triangulation) from the weak-field coefficient matrix, then records the target that turns that geometric computation into a Regge component comparison.
A triangulation $K$ is incidence-consistent when its combinatorial incidence data support well-defined dual weights. A concrete component comparison is the witness that those canonical incidence weights produce the expected second-order weak-field coefficient match (bilinear coefficient, row-sum, and off-diagonal component identities).
Upstream constants such as the dimensionless bridge ratio $K=\varphi^{1/2}$ appear in the broader calibration stack; here the local content is purely the geometric packaging of the component target.
proof idea
Definitional, not a proof. The body is the proposition $\forall K:\mathrm{Triangulation3D},;\mathrm{IncidenceConsistent}(K)\to\mathrm{Nonempty}(\mathrm{ConcreteComponentComparison},K)$. No tactics or lemmas are applied; the name simply freezes that universal claim as a reusable Prop for downstream discharge.
why it matters
This target is the hinge between the dual-weight geometry and the genuine component package. Downstream, finalReggeComponentTarget discharges it for canonical incidence/Laplacian second-order Regge data by exhibiting concreteComponentComparisonOfIncidence. Then genuine_component_package_of_final lifts any proof of the target to a nonempty GenuineComponentPackage on every incidence-consistent triangulation.
In the Recognition Science gravity line this closes the arbitrary-triangulation component step of the discrete Regge action, feeding the continuum weak-field match without fixing a particular mesh. It does not itself invoke T5–T8 or the RCL, but it is the geometric gate those continuum limits rely on once the component package is in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.