RECOGNITION SCIENCE: THE GRAVITY TEACHING MODELS Source snapshot: 17 September 2026 Companion to https://recognitionphysics.org/qg/ These notes explain the equations used by the lesson's controls and identify where the mathematical results stop and physical identifications begin. The JavaScript itself is available at /qg/gravity.js. 1. PERSISTENT PATTERN Example state: [2,1,0,-1,-2,-1,0,1]. Its mean is zero; its squared norm is 12. Update: new[i] = old[(i+1) mod 8]. This permutation conserves the mean and the sum of squared amplitudes. Eight applications return the original state. This is a real slice of the formal complex eight-slot cyclic-shift model. It is not a model of eight particles or a complete atomic calculation. Formal source: IndisputableMonolith/LightLanguage/Geometry/RecognitionDynamics.lean cyclicShift, cyclicShift_preserves_norm, cyclicShift_period_8 IndisputableMonolith/Gravity/LightMeaningProcessingBridge.lean voxelMeaningLoad (norm squared of the neutralized chord) The proposed matter interpretation is persistence of a light/recognition pattern. The cyclic-shift algebra proves the stated invariant, not that every physical object's microscopic dynamics is this permutation. 2. CLOCK AND DISTANCE READINGS The clock control supplies a constant rate ratio N. Over an observation window in which the reference counts 100 cycles, the other counts 100 N. Both use equal calibrated ticks. Count-bar length is proportional to accumulated cycles. No hand angle or cycle phase is inferred from the count ratio. Record-count shares can be used as a lapse (clock-rate) reading with physical clock and stationarity/window assumptions. An accumulated count ratio is not in general an instantaneous rate ratio. Network adjacency also does not give physical lengths. These are physical identifications to establish, not changes of variable that settle gravity. Formal source: IndisputableMonolith/Holography/RecordClockLapse.lean Definitions: share_i = rec_i / sum(rec); lapse_i = d share_i. The quotient-rule result distinguishes count shares from rate shares. The lesson's slider does not implement a density-to-clock law. 3. EXACT SPATIAL RESPONSE FROM THE J RULE J(x) = (x + 1/x)/2 - 1, x > 0. J(1)=0; J(x)=J(1/x); J(2)=J(1/2)=1/4. Its selection uses RS's specified apparatus/composition, regularity and normalization premises, not reciprocity alone. Published foundation: https://doi.org/10.3390/math14060935 Formal scope: RS-RUNG-1 certificate; IndisputableMonolith/VerdictMinimalNativeReporting.lean, Verdict.MinimalNativeReporting.recognition_science_native_reporting. The latter constructs a D3 witness on its selected apparatus; the lesson uses its normalized comparison-cost result, not universal metric selection. The displayed open chain has seven vertices i=0,...,6, fixed u_0=u_6=0, unit link weights and a specified positive centre source q. Its functional counts each edge ONCE: A(u) = sum_{i=0}^5 [cosh(u_{i+1}-u_i)-1] + q*u_3. Since J(exp(s))=cosh(s)-1, the link terms use the exact J cost. Write d=asinh(q/2). The minimizer is u_i=-d*min(i,6-i). Interior unsourced nodes have equal opposite fluxes. At the centre the stationarity equation is -2*sinh(d)+q=0. Convexity and the fixed endpoints make this the unique minimum. The endpoints provide boundary reaction; this is not a closed graph with a nonzero net source. The nudge slider changes only u_3. The displayed excess is A(u_nudged)-A(u_min). It does not show a relaxation or propagation law. Values are dimensionless, not physical height. The source coupling and boundary values are inputs. The additional clock bridge uses this SAME balanced u (before any nudge), with the ADOPTED physical identification Phi/c^2 = u/100. The first-order weak-field clock ratio relative to the endpoints is N = 1 + Phi/c^2; the displayed approximate cycle count per 100 endpoint cycles is 100+u. The display scale 1/100 is chosen, not derived. For q in [0,1.6], abs(Phi/c^2) <= 0.0221. Higher-order clock-rate terms are omitted. With equal positive physical spacing ell, the left and right slopes are respectively -c^2*d/(100*ell) and +c^2*d/(100*ell). Acceleration is the negative potential slope: rightward on the left, leftward on the right. At q=0 both slopes vanish. Arrows give direction, not trajectories or magnitude. Counts refer to held clocks; arrows refer to released test objects. The next local-frame experiment rescales the nonzero local acceleration to one, connecting this profile to CoherenceFall's cancellation result. The first-order N=1+Phi relation is the weak-field physical reading also used in RecordClockLapse.potential (dimensionless potential with c=1). The chain is not that account ledger, and no native derivation of this field-to-clock identification is claimed. Formal sources: IndisputableMonolith/Foundation/PairKernelExactJNonlinearGaussS13.lean exactJEdgeFlux = w_ij sinh(u_i-u_j) exactJNonlinearLaplacian = sum_j exactJEdgeFlux variation of the ORDERED-pair action = 2 sum_i du_i Laplacian_i stationarity is equivalent to its specified source equation. IndisputableMonolith/Gravity/ExactJStationaryMinimizer.lean exact-J strong tangent and stationary-source global-minimum results. The once-per-edge teaching chain uses the corresponding half action and source convention, with Dirichlet endpoints instead of closed-graph balance. The lesson-specific Lean audit also proves this exact five-variable fixed-endpoint minimum and its uniqueness, for all real q, using the strong cosh tangent inequality. Its declarations are GravityLessonValidation.chain_minimizes, chain_minimum_unique and source_parameter. Thus the stated seven-node minimum is checked directly, including the once-per-edge normalization and source sign. For small differences cosh(s)-1 = s^2/2 + O(s^4). The appropriately weighted 3D weak-field construction with matter coupling and refinement hypotheses recovers a Newton-Poisson response. It does not follow from a 1D chain alone. Published account: Simons, Allahyarov & Washburn, Entropy 28 (2026) 477, https://doi.org/10.3390/e28040477, especially section 4. Do not identify the potential locally with G times the density. Such a rule would have zero field on every exterior region where density vanishes and would not explain the exterior gravity of a body. The linked field problem is the response route illustrated here. 4. LOCAL COHERENT CONTINUATION / FREE FALL In the local weak-field model use upward height z. At the chosen centre, the potential has slope g. A downward frame acceleration a leaves the linear effective-potential term (g-a)z. The unique cancellation is a=g. The displayed normalized formula is phi_effective(z) = (1-a)z + k*z^2/2, z in {1,0,-1}. The optional tidal coefficient is k=0.6. The plotted horizontal marks are offsets proportional to phi_effective, exaggerated for readability; they are not laboratory clock measurements. At a=1 the linear part vanishes. The quadratic variation remains. With k nonzero, relative accelerations vary with z; no one frame acceleration cancels the field throughout. Formal source: IndisputableMonolith/Gravity/CoherenceFall.lean Its potential in a frame is phi(cm)+phi'(cm)*z+a_up*z; defect is abs(2*extent*(phi'(cm)+a_up)). Extent>0 gives the unique zero a_up=-phi'(cm). The page uses downward a, hence the opposite sign convention. This is a kinematic result for a supplied potential. It does not itself prove a source law, microscopic matter dynamics or quantum decoherence. 5. A SAME-ACTION MATTER SOURCE AND CURVATURE EXAMPLE An action is a common mathematical rule whose variation yields equations. The metric-dependent matter functional in SimplexMatterMetricAction.lean is S_m = kappa*V/2 * tr(G^-1 K), V=sqrt(|det G|)/24, where K is the real Gram matrix of transported matter differences. Full metric variation (including shear) gives T = kappa*(Q K Q - tr(QK)*Q/2), Q=G^-1, delta S_m = -V/2 tr(T delta G). The metric attachment and action are specified; this is a derived response within that construction, not a proof of native physical metric selection. A worked continuum extension uses the Lorentzian action int sqrt(|g|) [ gamma R/2 - kappa/2 sum_s g^{ab}D_a theta_s D_b theta_s - beta F^{ab}F_ab/4 ]. Two opposite phases theta_+=f(u), theta_-=-f(u) have cancelling gauge currents and adding stress T_uu=2 kappa f'(u)^2. Set A=0 and ds^2 = H du^2 - 2 du dv + dx^2 + dy^2, H = -kappa/gamma*f'(u)^2*(x^2+y^2) + P(u)*(x^2-y^2) + 2Q(u)*x*y. Then the full Einstein, phase and gauge equations hold in this specified continuum model. Ricci_uu=-(H_xx+H_yy)/2. The transverse tidal matrix is [kappa/gamma*f'^2 - P, -Q; -Q, kappa/gamma*f'^2 + P]. The teaching control sets kappa/gamma=1, f'=p and Q=0. Here phase means position within a repeating cycle, and p is its change per interval along the null wave coordinate u. The arithmetic readout shows the normalized signed currents p+(-p)=0 and source 2*p^2. The source contribution to the tidal trace is 2*p^2, shared equally between the two transverse directions. Arrows show relative acceleration -TidalMatrix times separation in the wave's affine coordinate. Their displayed scale is compressed uniformly; signs and relative directions come from this matrix. The ring does not depict integrated trajectories. P is a free wave datum, not radiation generated by the specified source. Source: MetricAttachmentAddendum.tex, draft 1.6, sections 4, 10-12; IndisputableMonolith/Gravity/CompactPhaseExactWave.lean, including metric_inverse, connection_eq, ricci_eq, einstein_eq, transverse_curvature, loweredStress_eq, sourced_equations. Lean source SHA256: 3eea75902dc4471c1cb395b11fc8e382b4906c0d0bba3debada99d9bc83e2651. Fresh lesson validation on 2026-09-17 rebuilt this module and its project dependencies and audited the named geometry, stress and sourced-equation proofs. Only propext, Classical.choice and Quot.sound occur in those axiom reports. These are Lean's standard logical axioms; explicit mathematical hypotheses and physical choices remain part of the statements. The Lean result is a pointwise chain of metric, derivative, curvature and stress identities. The smooth-profile realization and the phase/gauge equations are checked separately by symbolic differentiation, not by a Lean manifold-solution theorem. That existing symbolic check constructs all curvature components and checks the smooth profile's matter, Einstein and stress-divergence equations, with wrong-sign and wrong-factor controls. Scope: a selected common metric, gravitational Einstein action and coupling, and two phase copies are inputs. The native event-to-metric selection and complete coupled microscopic dynamics are still research targets. The wave solution is a concrete consistency construction, not an RS derivation of the Einstein action and not an asymptotically flat source-emission solution. 6. WHAT CONNECTS THE MODELS RS's organizing physical account: persistent matter activity; physical clock and distance comparisons; source-dependent spatial response; local coherent free continuation; coupled matter and geometry. Each displayed model makes a specific link precise. They are not one end-to-end microscopic simulation. Newtonian free fall and relativistic tidal curvature are recoveries/checks that an underlying account must connect, not uniquely RS observations. 7. VALIDATION AGAINST THE LEAN CODE, 17 SEPTEMBER 2026 The relevant source statements, definitions and proofs were read, then the lesson's six entry modules and the lattice quadratic audit were rebuilt on Lean 4.27.0-rc1, using the existing Mathlib dependency. A separate audit checks the named theorems' logical dependencies. The source manifest pins every project dependency used by these builds. This is a targeted audit, not a build of the entire research repository. Checked directly: - Eight-slot cyclic shift: conserved squared norm, preserved neutralized load and return after eight steps. - Clock comparison: the exact stationarity condition needed to interpret cumulative count shares as rate shares; a clock reading alone does not fix directional curvature. - Exact J field: action derivative, specified nonlinear source equation, global minimum, and the lesson-specific seven-node unique minimum. - Free fall: unique cancellation of the supplied potential's linear difference across an object of positive extent. The quadratic tidal illustration is additional algebra, not part of that linear theorem. - Matter response: full metric variation of the supplied action, including shear; constructed wave curvature and its sourced pointwise equations. - Software data: all 302 public rational coupling rows match the Lean table, and all 225 zero-order and 2,250 quadratic entries agree. Altered weight and momentum-offset controls are rejected. The quadratic Einstein-operator certificate is checked in Gravity.Analysis.KuhnCouplingTableQuadratic4D and its Audit module. The lab's full finite-momentum factorization and corrected off-shell quartic spectrum are separate exact Python/SymPy calculations. Their checks can be run on the page; they are not relabeled as Lean proofs. The physical identifications remain explicit: the source coupling, the chain-to-potential scale, the weak-field clock reading, the shared metric, the Einstein action and the wave's free polarization. Passing these proofs checks the mathematical statements with those inputs. It does not turn those inputs into a complete microscopic derivation of physical gravity. 17 SEPTEMBER AFTERNOON TEACHING ADDENDUM: DIRECTIONAL METRIC RESPONSE The geometry control reduces the actual definition S_m(kappa,K,G)=kappa/2 * sqrt(abs(det G))/24 * tr(G^-1 K) in Gravity/SimplexMatterMetricAction.lean. Choose kappa=48, G=diag(1,L^2,1,1), L>0, and K with just K_11=1 (horizontal) or K_22=1 (vertical), using zero-based coordinates. Thus detG=L^2, volume=L/24, S_horizontal=1/L, S_vertical=L. The fractional-stretch derivative L*dS/dL is respectively -1/L and L. The field's endpoint difference stays 1. The diagram is a rectangular coordinate cross-section; it does not depict the four-simplex itself. This is a positive-metric illustration of gradient and volume dependence, not a Lorentzian evolution or a solved matter-generated geometry. The full proved hasDerivAt_matterAction and metricWork results retain all metric directions. Metric attachment, matter interpolation and gravitational action remain specified physical ingredients of the coupled construction. The response sign is NOT the sign of gravitational attraction. Attraction in the source-chain example uses A=sum(cosh(delta u)-1)+q*u3, q>=0. Its negative central minimum, the adopted Phi/c^2=u/100, and a=-gradient Phi together give inward acceleration. Reciprocity of J alone does not fix the sign of this coupling or its normalization. Latest source inspected for the lesson's stated research boundary: MetricAttachmentAddendum.tex section22 (17 September 2026) derives an anisotropic original-clock field-strain response including longitudinal Gauss terms. Its conclusion still identifies the common physical strain law and geometry dynamics as the missing join to gravitational equations. This teaching page does not turn that result into a completed metric-selection claim and does not publish or redistribute the evolving research draft. CAUSAL-EXPLANATION ADDENDUM — 17 SEPTEMBER 2026 Energy balance and phase-driven motion This addendum documents two new teaching controls. It does not change the validation claims attached to the earlier code, or claim a fresh Lean build. The source files below were read directly. New browser/algebra checks are recorded separately with this revision's delivery evidence. A. From the native clock to a specified physical rate coupling IndisputableMonolith/Gravity/ExactJNativeRestEnergyWork.lean defines native rest energy as the actual Hamiltonian expectation, shows its nonnegativity and conservation, and proves that scaling a clock generator by N scales its evolution rate. The lapse matter energy is sum_i exp(-w_i) E_i, with native E_i >= 0. A positive dimensional conversion C multiplies the exact-J cost. The choice N=exp(-w), its universal physical use, and C are supplied inputs. The same file's dressed_clock_eigenvalue theorem preserves the frequencies under unitary conjugation: a change of representation is not rate slowing. ExactJPositiveMatterBackreaction.lean constructs the static minimizer for the specified exponential coupling on a finite mean-zero torus. B. Why the energy change is negative For the continuum weak-field teaching reduction, take smooth compact rest- energy density epsilon, positive stiffness K, and w -> 0 at infinity on R^3. The comparison-cost expansion gives F[w] = (K/2) integral |grad w|^2 - integral epsilon w, -K Delta w_* = epsilon. Integration by parts (with the decaying boundary) yields integral epsilon w_* = K integral |grad w_*|^2. Thus F[w_*] is minus the positive field energy. On the one-parameter family w=b w_*, choose a common energy unit Q=(K/2) integral |grad w_*|^2>0: field contribution/Q = b^2, matter energy CHANGE/Q = -2b, combined energy CHANGE/Q = b^2-2b = (b-1)^2-1. The binding-amount slider b in [0,2] uses these equations. The bars share fixed limits [-4,+4]. The source and field shape are held fixed; this is neither a solution of time-dependent field formation nor negative total matter energy. Weak amplitude is assumed even when b=2. The exact-J counterpart is in Gravity/ExactJPositiveMatterEnergy.lean: positive field energy tends to +1/2 integral |grad u|^2 while the coupled, background-subtracted binding energy tends to -1/2 integral |grad u|^2. That formal limit uses a mean-zero periodic setting with the source mean removed. It must not be misidentified with the different R^3 boundaries here. For two separated smooth positive sources on R^3, w_a=(-K Delta)^(-1)epsilon_a. Let C12=integral epsilon_1 w_2=integral epsilon_2 w_1 > 0. The field cross-energy is +C12; matter cross-change is -2 C12; the total interaction after subtracting isolated self-energies is -C12. For well-separated compact sources of rest energies E1,E2 this has leading term -E1 E2/(4 pi K r). It is exact outside non-overlapping spherical sources. The radial force is -dU/dr=-E1 E2/(4 pi K r^2). Self-energies of mathematical point sources are not used. The sign follows from positive stiffness and shared source/probe coupling. A consistent field-sign reversal cannot reverse it: a universal coupling enters the cross-interaction quadratically. The page's earlier exact chain uses u as a negative potential-like variable, with N approximately 1+u/100. This addendum uses w=-log N, positive near a positive source; to first order w=-u/100. Its exact-J stiffness conversion and spatial setting are not asserted to equal those of the illustrative chain. C. Phase gradient -> momentum -> acceleration Adopt the weak, nonrelativistic test-matter Hamiltonian H=p^2/(2m)+m c^2(N-1). In a uniform local gradient use z upward, g=c^2 dN/dz, remove the constant potential, and obtain H=p^2/(2m)+mgz. For any freely evolving packet psi_0, psi_g(z,t)=exp[-i(mgzt+mg^2t^3/6)/hbar] psi_0(z+g t^2/2,t) solves this linear-potential Schrödinger equation. Direct substitution checks the spatial derivative, translation and time-dependent common phase. Thus extra phase slope = -mgt/hbar, mean momentum change=-mgt, mean acceleration=-g, and mean fall distance=gt^2/2 for initial mean p=0. Wave spreading remains that of psi_0; no frozen packet or rigid matter model is assumed. The graph shows only the EXTRA phase tilt relative to the freely evolving translated packet, with common phase removed. Its horizontal axis is height and vertical axis is phase (positive up), never particle trajectory. The two line styles and all readouts distinguish masses 1 and m in [1,4]. With scaled units hbar=1, slopes and momenta are -gt and -mgt; both accelerations are -g. Values g in [0,1], t in [0,1.5] are display units chosen inside the weak/slow regime, not an assertion of order-one changes in N or velocities approaching c. At t=0 momentum change is zero but the acceleration need not be; at g=0 both vanish. These are continuum consequences of the stated Hamiltonian, not claims proved by the elementary eight-slot cyclic display. The shared mass coupling and inertial term are premises. The earlier CoherenceFall construction removes the supplied local timing slope by a frame acceleration; it supplies a consistent kinematic companion, not an independent microscopic derivation of this Hamiltonian. D. Scope of the causal explanation A. supplies a native clock energy and its exact scaling response. B. derives field balance and binding under the chosen clock coupling. C. explains the matter response for the supplied continuum Hamiltonian. The universal physical identification of this rate with every clock, distance and direction in one dynamical geometry remains a microscopic research target. The source and strain constructions elsewhere in the lesson are credited at their own specified-action scope. This scalar weak-field model is not the complete tensor theory, a full atom simulation, or the mechanism of gravitational-wave propagation. Newtonian force and equal test-body acceleration are recoveries; the phase-momentum law itself is ordinary quantum physics shared by RS.