Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPostingHostileProbe

show as:
view Lean formalization →

Hostile-probe module for Gap 2 non-equivariant posting: it shows the discrimination criterion is not vacuous. Using the already-known fact that incidence cost 1 fails to post mu on the two-bridge class, the probes force a numerator mass unequal to the orbit count. Gravity auditors cite it to confirm the witness criterion actually separates costs. The argument is a short family of discrimination lemmas on twists, orbits, and Gibbs mismatch.

claimThe Gap-2 discrimination criterion is non-vacuous: for the incidence cost of weight $1$, which is already known not to post $\mu$ on the two-bridge class, the Boltzmann numerator mass differs from the orbit count. Probe lemmas establish twist action on loop-and-bridge data, nontrivial orbits, non-Gibbs witnesses, and that a unit tilt breaks the identity.

background

Gap 2 concerns whether a letter cost posts the measure factor $\mu$ on bridge classes. For equivariant costs, posting is settled by a clean iff: the cost posts $\mu$ exactly when the Boltzmann numerator $\exp(-\mathrm{historyCost})$ is identically one, so the cost layer contributes no extra factor. That route explicitly leaves non-equivariant costs open; the parent module resolves them by a witness criterion rather than by the equivariant iff.

This module sits under that non-equivariant resolution. Its job is discrimination hygiene: a criterion that always returns the same answer is useless. The library already knows that incidence cost $1$ does not post $\mu$ at the two-bridge class, so any honest criterion must report a numerator mass different from the raw orbit count on that example.

Sibling probes name the concrete checks: twist moves on loop-and-bridge structure, nontrivial orbit, witness outside the Gibbs family, distinguishable probe family, and unit tilt breaking the identity map.

proof idea

Not a single theorem: a small battery of probe lemmas imported against the Gap-2 non-equivariant posting development. The spine is discrimination: feed incidence cost $1$ (already known not to post $\mu$ on the two-bridge class) into the criterion and obtain numerator mass $\neq$ orbit count. Supporting probes establish that twist acts nontrivially on loop-and-bridge data, that the relevant orbit is nontrivial, that the witness is not a Gibbs state, that the probe family is distinguishable, and that a unit tilt breaks the identity. Each is a short algebraic or rewriting argument against the parent posting definitions.

why it matters in Recognition Science

Closes a referee-facing hole in the Gap-2 non-equivariant posting story. The parent module supplies a witness criterion for costs outside the equivariant class (the case left open by the equivariant posting iff and exhibited by non-equivariant vertex-index costs). Without discrimination, that criterion could be a tautology. These probes pin that incidence cost $1$ forces a genuine numerator/orbit mismatch, so the criterion earns its keep in the Seven Gaps gravity ledger. No downstream modules are wired yet; the value is local soundness of the Gap-2 witness route.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)