Freudenthal4SimplexPathwiseSchlaefliTarget_open
plain-language theorem explainer
Records that the full Freudenthal 4-simplex pathwise Schläfli target is still open: the presence flag is false, so the Prop asserting it equals true is refuted. Gravity auditors cite it as a status witness that Gate-A2-style pathwise identity off the flat seed is not yet closed. The proof is a one-line Boolean inequality from the compiled flag.
Claim. It is not the case that the Freudenthal 4-simplex pathwise Schläfli target holds. Equivalently, the Boolean presence flag for that target is not $\mathrm{true}$ (so the target Prop, defined as equality of that flag to $\mathrm{true}$, fails).
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count are ten. Closed work already covers flat combinatorics, strictly positive flat hinge areas, the flat Schläfli summand table with vanishing column sums, seed-hinge dihedral derivatives along squared-edge paths, and flat directional Schläfli kill for every affine velocity through the flat seed.
The named target is a Prop wrapper around a Boolean presence flag: it holds exactly when that flag equals true. Module documentation lists the remaining open layer as the full pathwise identity off the flat seed on nondegenerate 4-simplices, remapped derivatives on every hinge row, elevation to a candidate, and 4D Einstein-Hilbert convergence of the RS action. This declaration is the explicit negation of the target Prop.
proof idea
Term-mode Boolean refutation. Assume the target Prop, which unfolds to the equality of the presence flag with true. That assumption yields false = true because the flag is compiled as false. Discharge by Bool.false_ne_true. No geometric lemmas are invoked; the proof only reads the flag.
why it matters
In the Recognition gravity stack this is a status seal, not a geometric advance. The module already proves the flat and directional Gate-A2-style inputs at the 4-simplex; the open list is the off-seed pathwise Schläfli identity and the elevation/convergence chain toward 4D continuum recovery. By proving the target Prop is false, the declaration prevents a silent claim that pathwise Schläfli is closed, matching the module rule that this work does not flip action-recovery gaps and does not inhabit a vacuous zero-measure Schläfli shell.
No downstream theorems currently depend on it (used_by is empty). Its role is audit hygiene: anyone reading the Freudenthal pathwise file sees a proved witness that the full pathwise target remains open, while the flat kernel, dihedral kernel, and Hessian assembly imports stay the active proved substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.