module module moderate

`IndisputableMonolith.Foundation.SimplicialLedger.DirichletAction`

Defines the weighted simplicial ledger graph and the discrete Dirichlet (Laplacian) action on vertex potentials. Supplies the pairing, bilinearity, and commutation identities that identify the quadratic action with an edge-sum of squared differences. Anyone working the discrete recognition ledger or continuum limit of the cost functional would cite it. The module is mostly definitions plus short algebraic identities proved by rearranging finite sums.

claimA weighted simplicial ledger is a finite vertex set with nonnegative edge weights $w_{ij}$. The discrete Laplacian action of a potential $\phi$ is $\frac12\sum_{i,j} w_{ij}(\phi_i-\phi_j)^2$, equivalently the pairing $\langle\phi,\Delta\phi\rangle$ of $\phi$ against its weighted graph Laplacian.

background

Recognition Science treats the ledger as a discrete substrate on which the J-cost and recognition composition law act. This module packages that substrate as a weighted simplicial graph: vertices carry real potentials, edges carry nonnegative weights, and the natural quadratic form is the Dirichlet energy of those potentials.

The discrete Laplacian $\Delta$ is the usual weighted degree-minus-adjacency operator. The Laplacian pairing and the bilinear form built from it are the polarization of the Dirichlet energy. Sibling lemmas record that the right-weighted sum is minus the left-weighted sum (skew-symmetry of oriented edges), that the pairing equals the left-weighted sum, and that the bilinear form coincides with the pairing and is symmetric.

The local setting is pure finite-dimensional real linear algebra over a finite index type; no continuum limit or forcing-chain step is taken here.

proof idea

This is primarily a definition module. WeightedLedgerGraph, discrete_laplacian, laplacian_pairing, laplacian_bilinear, and laplacian_action are introduced as data and quadratic forms. The supporting lemmas are short algebraic rewrites: expand double sums, factor weights, apply commutativity of multiplication and addition, and invoke linarith or ring where signs must cancel. No deep induction or external analytic input appears.

why it matters in Recognition Science

The Dirichlet action is the discrete skeleton of the recognition cost on the ledger: it is the quadratic form whose continuum limit and self-similar fixed-point analysis feed the forcing chain (J-uniqueness, phi, eight-tick structure). Downstream ledger and continuum-limit arguments need a clean identification of action equals pairing equals edge sum of squared differences; this module supplies those equalities in one place. It does not itself prove T5–T8, but it is the combinatorial substrate those steps sit on when the ledger is simplicial.

scope and limits

Does not define the J-cost or prove the Recognition Composition Law.
Does not force phi, the eight-tick period, or D = 3.
Does not treat infinite graphs, continuum limits, or spectral gaps.
Does not assign physical units or couple to mass or alpha formulae.
Does not claim uniqueness of the weights or of the vertex potentials.

declarations in this module (17)

structure WeightedLedgerGraph L25
def laplacian_action L31
def discrete_laplacian L36
def laplacian_pairing L40
def laplacian_bilinear L45
theorem right_weighted_sum_eq_neg_left L52
theorem pairing_eq_left_weighted_sum L85
theorem laplacian_bilinear_eq_pairing L110
theorem laplacian_bilinear_comm L149
theorem laplacian_pairing_comm L159
theorem laplacian_action_eq_pairing L167
theorem double_sum_mul_left L180
theorem laplacian_action_line_expansion L195
def unitDipole L253
theorem sum_mul_unitDipole L257
theorem laplacian_action_eq_potential_drop_of_eq_unitDipole L263
theorem laplacian_action_eq_half_potential_drop_of_two_eq_unitDipole L279