IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridge
Conditional hypothesis package for Gap2: from some shell onward, exact-path-class automorphisms rotate the discrete tick by +1 on the eight-tick fiber while preserving class mass. The hypothesis is not inhabited here; free-action search remains open. Downstream antipodal-balance and axiom-audit modules import it. The file defines the interface and derives mass-balance, oscillatory-tail, and endpoint-reversal consequences under that assumption.
claimConditional hypothesis: there exists a shell $N$ such that for all $n \ge N$, a family of exact-path-class automorphisms rotates the tick by $+1$ on $\mathrm{Fin}\,8$ and preserves the class measure $\mu$. Free-action search that would inhabit the hypothesis is open. Under the hypothesis one obtains eventual tick-fiber mass balance, an oscillatory tail (including a labeled form), exclusion of fixed points under tick shift, and an involutive endpoint reversal on the fiber.
background
Gap2 sits in the gravity seven-gaps program. The upstream enriched-carrier phase module attacks the continuum R5 residual: existence of a phase with oscillatory tail that is not the zero phase. That residual is the typed continuum substrate claim
$$\exists,\mathrm{phase},;\mathrm{OscillatoryTail}(\mathrm{phase})\land\neg\mathrm{OscillatoryTail}(0).$$
This bridge module packages the mechanical hypothesis that makes such a tail available from discrete data. The eight-tick octave (period $2^3$) supplies the fiber $\mathrm{Fin},8$. Class mass $\mu$ is the measure on exact path classes. A tail fiber shift is a family of exact-path-class automorphisms, from some shell $N$ onward, that add one to the tick coordinate and leave $\mu$ invariant.
Sibling material records elementary facts used under the hypothesis: successor on $\mathrm{Fin},8$ is never the identity; tick-fiber mass after a shift equals the predecessor mass (and vanishes only when the predecessor does); eventual balance of tick-fiber mass; oscillatory tail (plain and labeled); tick shift excludes fixed points, while a fixed class blocks the shift; and an involutive endpoint reversal ordered by the fiber.
proof idea
Definition-and-interface module, not a closed existence proof. The central object is the conditional TailFiberShift hypothesis (unhabited here). Remaining declarations are lemmas under that hypothesis or pure Fin-8 algebra: non-identity of $+1$ on the eight-tick fiber; transport of tick-fiber mass along the shift (successor and zero cases); eventual mass balance on fibers; derivation of oscillatory tail (and a labeled variant) from the shift; fixed-point exclusion versus fixed-class obstruction; and endpoint reversal with involutivity and order. No free-action witness is constructed; the open search is deferred.
why it matters in Recognition Science
Closes the sufficiency interface for Wave C / Gap2 R4–R5 work on oscillatory tails without claiming existence. The antipodal-balance bridge imports it to bank the mechanical half of the antipodal weakening: equal class mass on opposite Fin-8 fibers $p$ and $p+4$ from some shell onward. The dedicated audit module requires headline theorems to print inside [propext, Classical.choice, Quot.sound], so this file is the audited surface of the conditional bridge.
In the broader Recognition chain the eight-tick octave (T7) is the discrete clock; rotating the tick by one while preserving class mass is the minimal dynamical move that can force a non-trivial oscillatory tail on the continuum residual. Until free-action search inhabits the hypothesis, Gap2’s enriched-carrier phase attack remains conditional on this interface.
scope and limits
- Does not inhabit TailFiberShift; free-action search is explicitly open.
- Does not prove continuum oscillatory tail unconditionally; only under the shift hypothesis.
- Does not establish antipodal $p$ vs $p+4$ balance; that lives in the downstream bridge.
- Does not fix numerical gravity constants or mass-ladder rungs.
- Does not claim the hypothesis is forced by T0–T8 alone.
used by (2)
depends on (1)
declarations in this module (47)
-
structure
TailFiberShift -
lemma
fin8_add_one_ne -
theorem
tickFiberMass_succ_of_tailFiberShift -
theorem
tickFiberMass_eq_zero_of_tailFiberShift -
theorem
eventuallyTickFiberMassBalanced_of_tailFiberShift -
theorem
oscillatoryTail_of_tailFiberShift -
theorem
oscillatoryTail_of_labeled_tailFiberShift -
theorem
tick_shift_excludes_fixed_point -
theorem
fixed_class_blocks_tick_shift -
def
endpointReversal -
theorem
endpointReversal_involutive -
theorem
endpointReversal_ge -
def
tetSlotRotation -
theorem
tetSlotRotation_ge -
def
endpointReversalThenTetSlotRotation -
theorem
endpointReversalThenTetSlotRotation_ge -
def
allLoopsComplex -
theorem
endpointReversal_fixes_allLoops -
def
constTetComplex -
theorem
tetSlotRotation_fixes_constTet -
theorem
endpointReversalThenTetSlotRotation_fixes_constTet -
theorem
endpointReversalThenTetSlotRotation_fixes_allLoops -
theorem
endpointReversal_fixes_isolated -
theorem
tetSlotRotation_fixes_isolated -
theorem
endpointReversalThenTetSlotRotation_fixes_isolated -
def
endpointReversalClass -
theorem
endpointReversalClass_mk -
theorem
endpointReversalClass_involutive -
def
endpointReversalClassEquiv -
theorem
endpointReversalClass_fixes_isolatedClass -
def
tetSlotRotationClass -
def
tetSlotRotationInv -
theorem
tetSlotRotation_left_inv -
theorem
tetSlotRotation_right_inv -
theorem
tetSlotRotationInv_ge -
def
tetSlotRotationClassEquiv -
theorem
tetSlotRotationClass_fixes_isolatedClass -
def
endpointReversalThenTetSlotRotationClass -
def
endpointReversalThenTetSlotRotationClassEquiv -
theorem
endpointReversalThenTetSlotRotationClass_eq_equiv -
theorem
endpointReversalThenTetSlotRotationClass_fixes_isolatedClass -
theorem
endpointReversal_no_tailFiberShift -
theorem
tetSlotRotation_no_tailFiberShift -
theorem
endpointReversalThenTetSlotRotation_no_tailFiberShift -
structure
Gap2TailFiberShiftBridgeStatus -
def
gap2TailFiberShiftBridgeStatus -
theorem
gap2TailFiberShiftBridgeStatus_flags