foldT11Provenance
plain-language theorem explainer
String tag marking the fold construction's t11 orbit as arising from star-member cube offsets. Gravity analysts cite it when separating the fold t11 from the hybrid t11 as named objects. The body is a one-line string constant; no proof content.
Claim. The provenance label of the fold's $t_{11}$ orbit is the fixed string $\texttt{star\_member\_cube\_offsets}$.
background
Arc 2 step 9 task 1 asks whether the m² moment built from distinct hinge-edge origins is the m² moment of the exact flat cross-term fold as a functional of that fold's own symbol. Two t11 constructions appear: a hybrid route and a fold route. Their numerical moments agree at banked TT witnesses (both $-1/4$) and disagree off those witnesses, but agreement of values is not identity of definitions.
This module records only definitional status. Each construction carries a provenance string. The hybrid tag and the fold tag are different literals, so a global identity-of-definitions claim stays false. Witness equality is cited by certificate id from the resolved-star module and is not re-proved here.
The fold tag names the geometric origin of its t11 orbit: offsets of cube members inside the star. That naming is the sole content of this declaration.
proof idea
Definitional constant: the body is the string literal "star_member_cube_offsets". No tactics, no lemmas, no reduction.
why it matters
Supplies one side of the definitional mismatch used by t11_provenance_mismatch (hybrid tag ≠ fold tag, proved by decide) and by the composite step9_task1_status. That status packages four facts: provenance strings differ; naming link closed as definition is false; naming link closed at witnesses is true by citation; and the dictionary midpoint Bloch m² equals twice the hybrid moment at the TT-plus axis and symbol direction.
In the Recognition gravity stack this keeps honesty about the naming-link question: witness factor-2 measurements are evidence about moments, not a proof that the fold symbol and the hybrid construction are the same named object. It closes the definitional half of step 9 task 1 without reopening the resolved-star certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.