IndisputableMonolith.Gravity.Analysis.MetricEdgeImage4D
Defines the 4D metric-edge image on the unit hypercube (Freudenthal) patch: binary sites, patch displacements, edge strains, strain currents, and the Boolean set of admissible metric edges. Gravity analysts cite it when seating order-sensitive history-to-current maps or promoting discrete residuals to continuum form. Mostly definitional, with short algebraic lemmas on sign flip, symmetry, and one distinguished axis cross-term.
claimOn the unit 4-cube, sites are binary coordinates $s\in\{0,1\}^4$. From these one defines patch displacements, edge strains, and the strain current. The metric edge image is the Boolean set of admissible edge configurations realized by the discrete metric data. Basic identities include strain sign-flip under edge reversal and symmetry of displacement and current under the natural involution; a distinguished axis time-time cross term lies in the image.
background
The gravity analysis stack works on a 4D Freudenthal patch: the unit hypercube with binary site coordinates. Upstream, the pair-kernel / discrete Gauss lane supplies the continuity law that site-divergence of the recognition current equals local sigma-imbalance, and that the lattice integral of the source vanishes.
This module packages the discrete geometric carriers needed for edge-level gravity response: a $4\times 4$ matrix type, binary patch sites on the hypercube, patch displacements between sites, edge strain built from those displacements, and the associated strain current. The central object is the metric edge image, the Boolean set of edge configurations admitted by the discrete metric reading.
Notation is lattice-first and order-sensitive: later continuum modules replace bare Boolean non-membership in that image by a normalized-separation trichotomy under shape-regular refinement.
proof idea
Definition module, not a deep proof campaign. Core objects (matrix type, binary sites, displacements, edge strain, strain current, metric edge image) are introduced by direct constructors. Supporting lemmas are short algebraic identities: strain reverses sign under edge negation; displacement and strain current are symmetric under the natural involution; a named axis time-time cross configuration is shown to lie in the metric edge image; a zero-displacement identity at a fixed twelve-index pattern is recorded. No continuum limit or variational argument is attempted here.
why it matters in Recognition Science
Seats the discrete edge geometry that Campaign G2/G3 and G4/G5 read against. Downstream, OrderSensitiveHistoryResponse4D builds the order-sensitive history to edge-current response on the Freudenthal patch from depth-two commutator content, using this edge image as the admissible support. ContinuumOrderSensitiveResidual4D promotes the order-sensitive residual by replacing finite Boolean non-membership in the metric edge image with a normalized-separation trichotomy under a shape-regular refinement family. MetricEdgeImage4DAudit runs the axiom audit for the same carriers. In the broader RS gravity lane this is the discrete skeleton between pair-kernel flux and continuum residual claims; it does not itself force $D=3$ or the eight-tick octave.
scope and limits
- Does not prove a continuum limit or weak convergence of edge currents.
- Does not derive the discrete Gauss / sigma-imbalance law (imported upstream).
- Does not establish dynamical field equations or Einstein residuals.
- Does not classify all admissible edges beyond the named image and cross-term lemma.
- Does not address quantum or matter coupling on the patch.
used by (3)
depends on (1)
declarations in this module (17)
-
abbrev
Mat4 -
def
patchSite -
def
patchDisp -
def
edgeStrain -
def
strainCurrent -
def
MetricEdgeImage -
theorem
edgeStrain_neg -
theorem
patchDisp_symm -
theorem
strainCurrent_symm -
def
axisTTCross -
theorem
axisTTCross_in_MetricEdgeImage -
theorem
patchDisp_zero_twelve -
theorem
strainCurrent_axisTTCross_zero_twelve -
theorem
MetricEdgeImage_nontrivial -
theorem
elementaryPosting_zero_four_nonzero -
theorem
elementaryPosting_not_in_MetricEdgeImage -
theorem
zero_in_MetricEdgeImage