def definition def or abbrev

`Pattern`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  14def Pattern (n : Nat) := Fin n → Bool

proof body

Definition body.

  15
  16/-- Integer functional `Z` counting ones in a finite window. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

lambda_PBM_approx in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
ionization_monotone_within_period in IndisputableMonolith.Chemistry.IonizationEnergy decl_use
entries_distinct in IndisputableMonolith.CrossDomain.CrossPatternMatrix decl_use
anomaly_dissolved in IndisputableMonolith.Experimental.FlybyAnomaly decl_use
is_recognition_loop in IndisputableMonolith.Foundation.SimplicialLedger decl_use
recognition_loop_has_surjection in IndisputableMonolith.Foundation.SimplicialLedger decl_use
impulse_after_octaves_mono_decay in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_eq_eight in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_is_minimal_cover in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
VolcanicForcingAsJCostImpulseCert in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
utm_exists in IndisputableMonolith.Information.ChurchTuring decl_use
ledgerVecParity in IndisputableMonolith.LedgerParityAdjacency decl_use
parityPattern in IndisputableMonolith.LedgerParityAdjacency decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use
attempt5 in IndisputableMonolith.Mathematics.Euler decl_use
blockSumAligned8_periodic in IndisputableMonolith.Measurement decl_use
Cylinder in IndisputableMonolith.Measurement decl_use
firstBlockSum_eq_Z_on_cylinder in IndisputableMonolith.Measurement decl_use
observeAvg8_periodic_eq_Z in IndisputableMonolith.Measurement decl_use
Pattern in IndisputableMonolith.Measurement decl_use
subBlockSum8_periodic_eq_Z in IndisputableMonolith.Measurement decl_use
Z_of_window in IndisputableMonolith.Measurement decl_use
eight_tick_neutral_implies_exact in IndisputableMonolith.Measurement.WindowNeutrality decl_use
isNeutralWindow in IndisputableMonolith.Measurement.WindowNeutrality decl_use
eight_tick_minimal in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
C2_scope in IndisputableMonolith.Papers.ClaimBoundaries decl_use
C3_scope in IndisputableMonolith.Papers.ClaimBoundaries decl_use
card_pattern in IndisputableMonolith.Patterns decl_use
CompleteCover in IndisputableMonolith.Patterns decl_use
cover_exact_pow in IndisputableMonolith.Patterns decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

Z in IndisputableMonolith.Masses.Anchor decl_use
Pattern in IndisputableMonolith.Measurement decl_use
Pattern in IndisputableMonolith.Patterns decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
Pattern in IndisputableMonolith.Streams.Blocks decl_use